[wp/typed] fixed error when shifting a single value

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/oracle/mvar.0.res.oracle

@@ -10,15 +10,12 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
-Let x = A[0].
-Let a = 1[0].
 Assume {
-  Type: is_sint8(x).
   (* Heap *)
-  Type: IsArray1_sint8(A).
+  Have: linked(Malloc_0) /\ sconst(Mchar_0).
   (* Call 'Write' *)
-  Have: x = a.
+  Have: A[0] = 1.
 }
-Prove: P_equal(a, 1).
+Prove: P_equal(1, 1).
 
 ------------------------------------------------------------

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

@@ -10,15 +10,12 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
-Let x = A[0].
-Let a = 1[0].
 Assume {
-  Type: is_sint8(x).
   (* Heap *)
-  Type: IsArray1_sint8(A).
+  Have: linked(Malloc_0) /\ sconst(Mchar_0).
   (* Call 'Write' *)
-  Have: x = a.
+  Have: A[0] = 1.
 }
-Prove: P_equal(a, 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

@@ -6,49 +6,13 @@
   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] Failure: Error in why3:anomaly: Not_found
-  Raised at file "src/plugins/qed/term.ml", line 2716, characters 11-26
-  Called from file "src/plugins/wp/Definitions.ml", line 357, characters 16-33
-  Called from file "src/plugins/wp/Definitions.ml", line 376, characters 10-19
-  Called from file "list.ml", line 100, characters 12-15
-  Called from file "src/plugins/qed/term.ml", line 331, characters 21-35
-  Called from file "src/plugins/wp/ProverWhy3.ml", line 961, characters 2-9
-  Called from file "src/plugins/wp/ProverWhy3.ml", line 978, characters 17-57
-  Called from file "src/plugins/wp/ProverWhy3.ml", line 1258, characters 19-34
-  Called from file "src/plugins/wp/wpContext.ml", line 136, characters 17-20
-  Re-raised at file "src/plugins/wp/wpContext.ml", line 141, characters 23-32
-  Called from file "src/plugins/wp/ProverWhy3.ml", line 1255, characters 4-1023
-[kernel] Current source was: tests/wp_typed/mvar.i:14
-  The full backtrace is:
-  Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 532, characters 24-31
-  Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1098, characters 17-55
-  Called from file "src/kernel_services/plugin_entry_points/log.ml", line 525, characters 9-23
-  Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 528, characters 9-16
-  Called from file "src/plugins/wp/prover.ml", line 64, characters 2-34
-  Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
-  Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
-  Called from file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
-  Called from file "src/libraries/utils/task.ml", line 363, characters 14-36
-  Re-raised at file "src/libraries/utils/task.ml", line 369, characters 6-13
-  Called from file "src/libraries/utils/task.ml", line 463, characters 9-22
-  Called from file "array.ml", line 90, characters 31-48
-  Called from file "src/libraries/utils/task.ml", line 480, characters 4-45
-  Called from file "src/libraries/utils/task.ml", line 344, characters 14-18
-  Called from file "src/plugins/wp/register.ml", line 717, characters 4-35
-  Called from file "src/plugins/wp/register.ml", line 816, characters 8-23
-  Called from file "src/libraries/stdlib/extlib.ml", line 343, characters 14-17
-  Re-raised at file "src/libraries/stdlib/extlib.ml", line 343, characters 41-48
-  Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
-  Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
-  Called from file "queue.ml", line 105, characters 6-15
-  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
-  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
-  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
-  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
-  
-  Plug-in wp aborted: internal error.
-  Please report as 'crash' at http://bts.frama-c.com/.
-  Your Frama-C version is 19.1+dev (Potassium).
-  Note that a version and a backtrace alone often do not contain enough
-  information to understand the bug. Guidelines for reporting bugs are at:
-  http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
+[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%
+-------------------------------------------------------------