Merge branch 'feature/wp/fix-ref-usage' into 'master'

Feature/wp/fix ref usage

See merge request frama-c/frama-c!2403

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

src/plugins/wp/tests/wp_typed/mvar.i

+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;
+}

src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json

+{ "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 } } } } }

src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/895ce5c124c30552810b4458d89f3885.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0081,
+  "steps": 6 }

src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/e5ffef57a0640be83d7c30f0890f6022.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0089,
+  "steps": 5 }

src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle

+# 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%
+-------------------------------------------------------------