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 2a8e1c460523dc755e0fff4f132f7358d51ead8b..969326b6fe91bdce835b6efaa34b84929f0936da 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 0000000000000000000000000000000000000000..d2b0d3de19a44706760e2805d7c14e3c949490cf
--- /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 0000000000000000000000000000000000000000..9c2dfad26f93af7de878b0d812d73f6cfaefc23d
--- /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 0000000000000000000000000000000000000000..f2a27e3b194a6c9b7d4b28557390cf44a082e05a
--- /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 a9310f3d13966a1a1a987551a3cfb57c72a1e8cd..347be3b9000ef396daebdf2335c9f2fbaad88a84 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 a5b7496b8bcac1057fc2ee1bfc1baa80fad18099..a5416d5a156584963cf2cf5bcc42ebfb7e27b602 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 6defa5bcd74401f918dc86a7cc117daec22e3cc0..6a684ed4e4fa19eaae36dd09d3b7717df0c65a0e 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 07c88e21be0523b36d4e4beb3bc08582fc5171d3..578ffb9958aef6bacf33cb5680b0ecbafe0f5efe 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 6f266473c3da74f3125a63e16abeffe0f28b841c..72b93b5526df3a049e39f88a0d1809d9e3ec6941 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 33301d71a33e5ae00a155943d5cecf22939281b0..09755e2c851424c8871e943d93a05b0253bf1db9 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 b729e0fa94298a8357840d6070954d28886407f2..706eac2712b2643fdff1c6caaea6ca9725f711ad 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 2580abd19c2c0e2e65e4a8eab92f30bf4b298b28..d035bcd5046d5abb9450a6bd66795f980f87369f 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 } ] } } ]