[wp] fix triggers for cint ranges

f609aa83 · Loïc Correnson · Virgile Prevosto · 70760544 · f609aa83 · f609aa83
Commit f609aa83 authored Nov 26, 2020 by Loïc Correnson Committed by Virgile Prevosto Nov 26, 2020
--- 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 * **)


--- a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
+# 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.
+
+------------------------------------------------------------
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
+# 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%
+------------------------------------------------------------
--- a/src/plugins/wp/tests/wp_plugin/overflow2.c
+++ b/src/plugins/wp/tests/wp_plugin/overflow2.c
+/* 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);
+}
--- 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 } ] } } ]
--- 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 } ] } } ]
--- 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,

--- 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 } ] } } ]
--- 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 } ] } } ]
--- 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 } ] } } ]
--- 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 } ] } } ]
--- 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 } ] } } ]