From 3edbdbf0d2214d4133e358bf62af15313e59d203 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 3 Oct 2019 17:00:44 +0200
Subject: [PATCH] [wp/typed] fixed error when shifting a single value
---
src/plugins/wp/RefUsage.ml | 35 ++++++++----
.../tests/wp_typed/oracle/mvar.0.res.oracle | 9 +--
.../tests/wp_typed/oracle/mvar.1.res.oracle | 9 +--
.../wp_typed/oracle_qualif/mvar.0.report.json | 14 +++++
.../895ce5c124c30552810b4458d89f3885.json | 2 +
.../e5ffef57a0640be83d7c30f0890f6022.json | 2 +
.../wp_typed/oracle_qualif/mvar.res.oracle | 56 ++++---------------
7 files changed, 59 insertions(+), 68 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/895ce5c124c30552810b4458d89f3885.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.session/cache/e5ffef57a0640be83d7c30f0890f6022.json
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index eedd0bb9bea..894b937dc12 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/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index 89f9259c209..b290830da12 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/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).
------------------------------------------------------------
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
index cf4e0cdda57..c5ee1a264cf 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/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).
------------------------------------------------------------
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 00000000000..5d34a2aa148
--- /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 00000000000..5230d4cfc10
--- /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 00000000000..8722bffd2aa
--- /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
index d8be2b42eba..48f19a88154 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/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%
+-------------------------------------------------------------
--
GitLab