From f609aa83f209cade3d1eb2a12ced0a72c00f83d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 26 Nov 2020 11:36:26 +0100
Subject: [PATCH] [wp] fix triggers for cint ranges
---
src/plugins/wp/share/why3/frama_c_wp/cint.mlw | 16 +--
.../wp_plugin/oracle/overflow2.res.oracle | 106 ++++++++++++++++++
.../oracle_qualif/overflow2.res.oracle | 27 +++++
src/plugins/wp/tests/wp_plugin/overflow2.c | 44 ++++++++
.../init_t2_bis_v2_loop_assigns_part2.json | 4 +-
.../init_t2_bis_v2_loop_assigns_part3.json | 4 +-
.../init_t2_v2_loop_assigns_2_part2.json | 2 +-
.../init_t2_v2_loop_assigns_2_part3.json | 4 +-
.../script/init_t2_v2_loop_assigns_part2.json | 4 +-
.../script/init_t2_v2_loop_assigns_part3.json | 4 +-
.../script/init_t2_v3_loop_assigns_part2.json | 4 +-
.../script/init_t2_v3_loop_assigns_part3.json | 2 +-
12 files changed, 199 insertions(+), 22 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/overflow2.c
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
index 2a8e1c46052..969326b6fe9 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
@@ -102,14 +102,14 @@ theory Cint
meta "remove_for_" lemma is_to_uint
meta "remove_for_" lemma is_to_sint
- axiom is_to_uint8 : forall x:int [ is_uint8(to_uint8 x) ]. is_uint8 (to_uint8 x)
- axiom is_to_sint8 : forall x:int [ is_sint8(to_sint8 x) ]. is_sint8 (to_sint8 x)
- axiom is_to_uint16 : forall x:int [ is_uint16(to_uint16 x) ]. is_uint16 (to_uint16 x)
- axiom is_to_sint16 : forall x:int [ is_sint16(to_sint16 x) ]. is_sint16 (to_sint16 x)
- axiom is_to_uint32 : forall x:int [ is_uint32(to_uint32 x) ]. is_uint32 (to_uint32 x)
- axiom is_to_sint32 : forall x:int [ is_sint32(to_sint32 x) ]. is_sint32 (to_sint32 x)
- axiom is_to_uint64 : forall x:int [ is_uint64(to_uint64 x) ]. is_uint64 (to_uint64 x)
- axiom is_to_sint64 : forall x:int [ is_sint64(to_sint64 x) ]. is_sint64 (to_sint64 x)
+ axiom is_to_uint8 : forall x:int. is_uint8 (to_uint8 x)
+ axiom is_to_sint8 : forall x:int. is_sint8 (to_sint8 x)
+ axiom is_to_uint16 : forall x:int. is_uint16 (to_uint16 x)
+ axiom is_to_sint16 : forall x:int. is_sint16 (to_sint16 x)
+ axiom is_to_uint32 : forall x:int. is_uint32 (to_uint32 x)
+ axiom is_to_sint32 : forall x:int. is_sint32 (to_sint32 x)
+ axiom is_to_uint64 : forall x:int. is_uint64 (to_uint64 x)
+ axiom is_to_sint64 : forall x:int. is_sint64 (to_sint64 x)
(** * C-Integer Conversions are identity when in-range * **)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
new file mode 100644
index 00000000000..d2b0d3de19a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
@@ -0,0 +1,106 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/overflow2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function pointers_and_companions
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'pointers_and_companions':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 21):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 23):
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
+ (* Pre-condition *)
+ Have: p1_off_0 <= 10.
+}
+Prove: (p1_off_0 + to_uint16(distance_0)) <= 65545.
+
+------------------------------------------------------------
+
+Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 24):
+Let x = p1_off_0 + to_uint16(distance_0).
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
+ (* Pre-condition *)
+ Have: p1_off_0 <= 10.
+ (* Assertion 'a04' *)
+ Have: x <= 65545.
+}
+Prove: x = to_uint32(x).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 14) in 'pointers_and_companions':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function pointers_and_companions_ulong
+------------------------------------------------------------
+
+Goal Post-condition 'postul' in 'pointers_and_companions_ulong':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 39):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 40):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 41):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 42):
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+ (* Pre-condition *)
+ Have: p1_off_alt_0 <= 10.
+}
+Prove: (p1_off_alt_0 + to_uint16(distance_0)) <= 65545.
+
+------------------------------------------------------------
+
+Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 43):
+Let x = p1_off_alt_0 + to_uint16(distance_0).
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+ (* Pre-condition *)
+ Have: p1_off_alt_0 <= 10.
+ (* Assertion 'a09' *)
+ Have: x <= 65545.
+}
+Prove: x = to_uint32(x).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 33) in 'pointers_and_companions_ulong':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
new file mode 100644
index 00000000000..9c2dfad26f9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
@@ -0,0 +1,27 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/overflow2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 14 goals scheduled
+[wp] [Qed] Goal typed_pointers_and_companions_ensures_post : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a01 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a02 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a03 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_assert_a04 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_assert_a05 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assigns : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_ensures_postul : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a06 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a07 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a08 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_ulong_assert_a09 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_ulong_assert_a10 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assigns : Valid
+[wp] Proved goals: 14 / 14
+ Qed: 10
+ Alt-Ergo: 4
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ pointers_and_companions 5 2 7 100%
+ pointers_and_companions_ulong 5 2 7 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/overflow2.c b/src/plugins/wp/tests/wp_plugin/overflow2.c
new file mode 100644
index 00000000000..f2a27e3b194
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/overflow2.c
@@ -0,0 +1,44 @@
+/* run with: frama-c-gui -wp -wp-rte strange_work_again.c */
+// uproven: a04, a05, a09, a10
+// note that when the type of distance is ushort, all is proven
+
+typedef unsigned char uchar;
+typedef unsigned short ushort;
+typedef unsigned int uint;
+typedef unsigned long ulong;
+
+uint p1_off, p2_off;
+
+/*@
+ requires p1_off <= 10;
+ assigns p2_off;
+ ensures post: p2_off == p1_off + (ushort)distance;
+*/
+void pointers_and_companions(short distance)
+{
+ p2_off = p1_off + (ushort)distance;
+ //@ assert a01: p2_off == (uint)(p1_off + (ushort)distance);
+ //@ assert a02: (ushort)distance <= 65535;
+ //@ assert a03: p1_off <= 10;
+ //@ assert a04: p1_off + (ushort)distance <= 10 + 65535;
+ //@ assert a05: p1_off + (ushort)distance == (uint)(p1_off + (ushort)distance);
+}
+
+// the same behavior for ulong
+
+ulong p1_off_alt, p2_off_alt;
+
+/*@
+ requires p1_off_alt <= 10;
+ assigns p2_off_alt;
+ ensures postul: p2_off_alt == p1_off_alt + (ushort)distance;
+*/
+void pointers_and_companions_ulong(short distance)
+{
+ p2_off_alt = p1_off_alt + (ushort)distance;
+ //@ assert a06: p2_off_alt == (uint)(p1_off_alt + (ushort)distance);
+ //@ assert a07: (ushort)distance <= 65535;
+ //@ assert a08: p1_off_alt <= 10;
+ //@ assert a09: p1_off_alt + (ushort)distance <= 10 + 65535;
+ //@ assert a10: ((ulong)(p1_off_alt + (ushort)distance)) == (p1_off_alt + (ushort)distance);
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index a9310f3d139..347be3b9000 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0236,
+ "verdict": "valid", "time": 0.0241,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0251,
+ "verdict": "valid", "time": 0.025,
"steps": 41 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index a5b7496b8bc..a5416d5a156 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.018,
+ "verdict": "valid", "time": 0.0199,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.022,
+ "verdict": "valid", "time": 0.0241,
"steps": 29 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 6defa5bcd74..6a684ed4e4f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0177,
+ "verdict": "valid", "time": 0.0202,
"steps": 40 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index 07c88e21be0..578ffb9958a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0154,
+ "verdict": "valid", "time": 0.0143,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0157,
+ "verdict": "valid", "time": 0.0146,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 6f266473c3d..72b93b5526d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.016,
"steps": 33 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0171,
+ "verdict": "valid", "time": 0.0161,
"steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index 33301d71a33..09755e2c851 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.016,
"steps": 33 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0171,
+ "verdict": "valid", "time": 0.0161,
"steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index b729e0fa942..706eac2712b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0169,
+ "verdict": "valid", "time": 0.0209,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.0184,
"steps": 39 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 2580abd19c2..d035bcd5046 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -6,5 +6,5 @@
"verdict": "valid", "time": 0.0146,
"steps": 27 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0146,
+ "verdict": "valid", "time": 0.0143,
"steps": 27 } ] } } ]
--
GitLab