[WP] fixes some points about \exit_status

src/plugins/wp/LogicSemantics.ml

@@ -912,7 +912,7 @@ struct
 
   let assignable_lval env ~unfold lv =
     match fst lv with
-    | TResult _ -> [] (* special case ! *)
+    | TResult _  | TVar{lv_name="\\exit_status"} -> [] (* special case ! *)
     | _ ->
         let offsets =
           let obj = Ctypes.object_of_logic_type (Cil.typeOfTermLval lv) in

src/plugins/wp/RefUsage.ml

@@ -449,7 +449,7 @@ and term (env:ctx) (t:term) : model = match t.term_node with
 
 (* --- Lvalues --- *)
 and term_lval env (h,ofs) = match h with
-  | TResult _ -> nothing
+  | TResult _ | TVar{lv_name="\\exit_status"} -> nothing
   | TVar( {lv_origin=None ; lv_kind=LVLocal} as lvar) ->
       (* var bound by a \\let *)
       load (term_offset env (get_tlet env.local lvar) ofs)
@@ -470,6 +470,8 @@ and term_offset env (l:model) = function
 
 and addr_lval env (h,ofs) = match h with
   | TResult _ -> Wp_parameters.abort ~current:true "Address of \\result"
+  | TVar{lv_name="\\exit_status"} ->
+      Wp_parameters.abort ~current:true "Address of \\exit_status"
   | TMem t -> term_offset env (term env t) ofs
   | TVar( {lv_origin=Some x} ) -> term_offset env (Loc_var x) ofs
   | TVar( {lv_origin=None} as x ) ->

src/plugins/wp/normAtLabels.ml

@@ -65,7 +65,7 @@ class norm_at (mapping : label_mapping) =
       | TAddrOf (h, _) | TLval (h, _) | TStartOf (h, _)  ->
           let old_label = current_label in
           let at_label = match h with
-            | TResult _ -> Some Clabels.post
+            | TResult _ | TVar{lv_name="\\exit_status"} -> Some Clabels.post
             | _ -> old_label
           in
           current_label <- None;