diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index eedd0bb9bea3416e5a53a9115a85568179c2a4ce..894b937dc129c5c34a7458f0d21ee0b5eaeb36b7 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -145,6 +145,16 @@ type model =
| Val_comp of varinfo * value (* x.f[_].g... *)
| Val_shift of varinfo * value (* (x + E) *)
+[@@@ warning "-32" ]
+let pp_model fmt = function
+ | E v -> E.pretty fmt v
+ | Loc_var x -> Format.fprintf fmt "&%a" Varinfo.pretty x
+ | Loc_shift(x,v) -> Format.fprintf fmt "&%a.(%a)" Varinfo.pretty x E.pretty v
+ | Val_var x -> Varinfo.pretty fmt x
+ | Val_comp(x,v) -> Format.fprintf fmt "%a.(%a)" Varinfo.pretty x E.pretty v
+ | Val_shift(x,v) -> Format.fprintf fmt "%a+(%a)" Varinfo.pretty x E.pretty v
+[@@@ warning "+32" ]
+
let nothing = E E.bot
let v_model v = if E.is_bot v then nothing else E v
@@ -203,8 +213,12 @@ let field = function
| m -> shift m E.bot
let load = function
- | Loc_var x -> Val_var x
- | Loc_shift(x,e) -> E (E.access x ByValue e)
+ | Loc_var x -> Val_var x (* E.access x ByValue E.bot *)
+ | Loc_shift(x,e) ->
+ if Cil.isArithmeticOrPointerType x.vtype then
+ E (E.access x ByAddr e)
+ else
+ E (E.access x ByValue e)
| Val_var x -> E (E.access x ByRef E.bot)
| Val_comp(x,e) -> E (E.access x ByRef e)
| Val_shift(x,e) -> E (E.access x ByArray e)
@@ -693,17 +707,17 @@ let param a m = match a with
| ByArray -> e_value (load (shift m E.bot))
let update_call_env (env:global_ctx) v =
- let r,differ = E.cup_differ env.code v
- in env.code <- r ;
- differ
+ let r,differ = E.cup_differ env.code v in
+ env.code <- r ; differ
let call_kf (env:global_ctx) (formals:access list) (models:model list) (reached:bool) =
let unmodified = ref reached in
let rec call xs ms = match xs, ms with
- | [] , _ | _ , [] -> ()
| x::xs , m::ms ->
- if update_call_env env (param x m) then unmodified := false;
+ let actual = param x m in
+ if update_call_env env actual then unmodified := false;
call xs ms
+ | _ -> ()
in call formals models;
!unmodified
@@ -748,10 +762,11 @@ let compute_usage () =
in
(* update from accesses of formals of the called spec for each calls*)
let specs_formals = called.spec_formals in
- let formals = Kernel_function.get_formals called_kf in
- let formals = List.map (fun vi -> E.get vi specs_formals) formals in
+ let params = Kernel_function.get_formals called_kf in
+ let formals = List.map (fun vi -> E.get vi specs_formals) params in
let kf_call reached call = call_kf env formals call reached in
- List.fold_left kf_call reached calls in
+ List.fold_left kf_call reached calls
+ in
state_fp.todo <- KFmap.remove kf state_fp.todo ;
let cphi = env.cphi in
let reached = KFmap.fold kf_calls cphi true in
diff --git a/src/plugins/wp/tests/wp_typed/mvar.i b/src/plugins/wp/tests/wp_typed/mvar.i
new file mode 100644
index 0000000000000000000000000000000000000000..396b66373edf0915c76759110eedfd8ce1b64240
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/mvar.i
@@ -0,0 +1,20 @@
+extern char A[20];
+
+//@ predicate equal(integer x,integer y) = x==y ;
+
+/*@
+ ensures \forall integer i ; 0 <= i < n ==> \at( A[i] == *(p + i) , Pre);
+ */
+extern void Write(char *p, int n);
+
+
+/*@
+ ensures equal(A[0],1) ;
+ */
+void Job(void)
+{
+ char DataWrite;
+ DataWrite = 1 ;
+ Write((& DataWrite),1);
+ return;
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b290830da12f38bd7a0be3610f09ae4b77108df9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_typed/mvar.i:14: Warning:
+ No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function Job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
+Assume {
+ (* Heap *)
+ Have: linked(Malloc_0) /\ sconst(Mchar_0).
+ (* Call 'Write' *)
+ Have: A[0] = 1.
+}
+Prove: P_equal(1, 1).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c5ee1a264cf0f1bb92bd2c8d9ea4c9ff09c56a40
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_typed/mvar.i:14: Warning:
+ No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function Job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
+Assume {
+ (* Heap *)
+ Have: linked(Malloc_0) /\ sconst(Mchar_0).
+ (* Call 'Write' *)
+ Have: A[0] = 1.
+}
+Prove: P_equal(1, 1).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
new file mode 100644
index 0000000000000000000000000000000000000000..5d34a2aa148ec69a768c4de87205861440f6366d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 1 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "wp:functions": { "Job": { "Job_ensures": { "why3:Alt-Ergo,2.0.0":
+ { "total": 1, "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/895ce5c124c30552810b4458d89f3885.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/895ce5c124c30552810b4458d89f3885.json
new file mode 100644
index 0000000000000000000000000000000000000000..5230d4cfc10fead23aa88fcd978ebb16058ac3bb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/895ce5c124c30552810b4458d89f3885.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0081,
+ "steps": 6 }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/e5ffef57a0640be83d7c30f0890f6022.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/e5ffef57a0640be83d7c30f0890f6022.json
new file mode 100644
index 0000000000000000000000000000000000000000..8722bffd2aab5ce648cc2e4e69a78617a55cc0c6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/e5ffef57a0640be83d7c30f0890f6022.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0089,
+ "steps": 5 }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..48f19a88154aac3ef6ba18614891f4c87c71fdaa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_typed/mvar.i:14: Warning:
+ No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo 2.0.0] Goal typed_Job_ensures : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Alt-Ergo 2.0.0: 1
+[wp] Report in: 'tests/wp_typed/oracle_qualif/mvar.0.report.json'
+[wp] Report out: 'tests/wp_typed/result_qualif/mvar.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+Job - 1 (1..12) 1 100%
+-------------------------------------------------------------