From 413f59801a6ee33971c17359b5060d66c09788cd Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 26 Jul 2019 10:32:41 +0200
Subject: [PATCH] [WP] fixes some points about \exit_status
---
src/plugins/wp/LogicSemantics.ml | 2 +-
src/plugins/wp/RefUsage.ml | 4 +++-
src/plugins/wp/normAtLabels.ml | 2 +-
3 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 03a54a044be..52ad3beab41 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 47761ae4794..38647c7e307 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 1cdc9f56cb6..c876927da3c 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;
--
GitLab