diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 03a54a044beacc6bab9052703abd4325d92d37c2..52ad3beab41cc463a048aa1743a95bb55a318b2f 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/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
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 47761ae47948df4498381eb8585b49be6b1e94c1..38647c7e307cf9b980f174c82d078a23d1ebe8d6 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/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 ) ->
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 1cdc9f56cb6bab7402b7a4c9827a77fa0ed8766e..c876927da3c546f5a455079e05aba5710743e281 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/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;