[kernel] \exit_status is a special case for ast diff

src/kernel_services/ast_queries/ast_diff.ml

@@ -646,9 +646,22 @@ and is_matching_logic_var lv lv' env =
      | None ->
        (match Logic_var.find lv with
         | `Not_present -> false
-        | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''))
+        | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+        | exception Not_found ->
+          if lv.lv_name = "\\exit_status" && lv'.lv_name = "\\exit_status"
+          then begin Logic_var.add lv (`Same lv'); true end
+          else begin
+            match logic_var_correspondance lv env with
+            | None -> false
+            | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+          end))
   | _ -> false
 
+and logic_var_correspondance lv env =
+  match find_candidate_logic_var lv env with
+  | None -> None
+  | Some lv' -> Logic_var.add lv (`Same lv'); Some lv'
+
 and is_same_term_offset lo lo' env =
   match lo, lo' with
   | TNoOffset, TNoOffset -> true
@@ -1212,6 +1225,16 @@ and logic_vars_env l l' env =
   else
     false, env
 
+and find_candidate_logic_var ?loc:_loc lv env =
+  let candidates = Logic_env.find_all_logic_functions lv.lv_name in
+  match List.find_opt (fun li -> li.l_profile = []) candidates with
+  | None -> Format.printf "No such var@."; None
+  | Some li ->
+    Format.printf "Found something@.";
+    if is_same_logic_var lv li.l_var_info env then
+      Some li.l_var_info
+    else None
+
 (* because of overloading, we have to check for a corresponding profile,
    leading to potentially recursive calls to is_same_* functions. *)
 and find_candidate_logic_info ?loc:_loc li env =

tests/syntax/ast_diff_1.i

@@ -45,6 +45,7 @@ int has_static_local(void) {
   return x;
 }
 
+/*@ exits \exit_status == 1; */
 int decl(void);
 
 int used_in_decl;

tests/syntax/ast_diff_2.i

@@ -46,6 +46,7 @@ int has_static_local(void) {
 
 int used_in_decl;
 
+/*@ exits \exit_status == 1; */
 int decl() {
   used_in_decl++;
   return used_in_decl;