diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index 869eff6a1b7f6cd18dce59aa2f9d702dfb98fed6..bb01a2849ae1025520d5aaee65f675a7798cd87c 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -wp-prop=CHECK,FAILS
+ COMMENT:
*/
/* run.config_qualif
- OPT: -wp-prop=CHECK,FAILS -wp-timeout 20
+ OPT: -wp-prop=-FAILS -wp-timeout 25
*/
struct S {
@@ -14,12 +14,13 @@ void initialize(void){
struct S s ;
s.i = 0 ;
/*@
- loop invariant CHECK: 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
- loop assigns CHECK: i, s.a[0 .. 9];
+ loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
+ loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
- //@ check CHECK: \initialized(&s);
+ //@ check \initialized(&s);
}
void range(void){
@@ -28,17 +29,19 @@ void range(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@
- loop invariant CHECK: \initialized(&s);
- loop assigns CHECK: i, s.a[1 .. 4];
+ loop invariant \initialized(&s);
+ loop assigns i, s.a[1 .. 4];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i){
if(1 <= i && i <= 4) s.a[i] = 1 ;
}
- //@ check CHECK: \initialized(&s);
+ //@ check \initialized(&s);
}
void field(void){
@@ -47,10 +50,14 @@ void field(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
- /*@ loop assigns CHECK: i, s.i; */
+ /*@
+ loop assigns i, s.i;
+ loop variant 10-i;
+ */
for(int i = 0; i < 10; ++i){
s.i++;
}
@@ -63,12 +70,14 @@ void array(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@
loop invariant 0 <= i <= 10;
- loop assigns CHECK: i, s.a[0..9];
+ loop assigns i, s.a[0..9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i){
s.a[i] = 1 ;
@@ -82,10 +91,14 @@ void index(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
- /*@ loop assigns CHECK: i, s.a[4]; */
+ /*@
+ loop assigns CHECK: i, s.a[4];
+ loop variant 10-i;
+ */
for(int i = 0; i < 10; ++i){
if(i == 4) s.a[i] = 1 ;
}
@@ -98,17 +111,19 @@ void descr(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i ;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@
- loop invariant CHECK: \initialized(&s);
- loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } };
+ loop invariant \initialized(&s);
+ loop assigns i, { s.a[i] | integer i ; i \in { 0, 2, 4 } };
+ loop variant 10-i ;
*/
for(int i = 0; i < 10; ++i){
if(i == 0 || i == 2 || i == 4) s.a[i] = 1 ;
}
- //@ check CHECK: \initialized(&s);
+ //@ check \initialized(&s);
}
void comp(void){
@@ -117,12 +132,14 @@ void comp(void){
/*@
loop invariant 0 <= i <= 10 && \initialized(&s.a[0 .. i-1]);
loop assigns i, s.a[0 .. 9];
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@
loop invariant 0 <= i <= 10 ;
- loop assigns CHECK: i, s;
+ loop assigns i, s;
+ loop variant 10-i;
*/
for(int i = 0; i < 10; ++i){
s.a[i] = 1 ;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index 1a871701efc341f13212353d4d635dde6922232f..dd43d73c6a48a82c410a2fe7be036e1fb34921e2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -1,12 +1,57 @@
# frama-c -wp [...]
[kernel] Parsing assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal comp_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal comp_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal descr_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal descr_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal field_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal field_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal index_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal index_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal initialize_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal initialize_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal range_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal range_terminates (Cfg) (Trivial)
------------------------------------------------------------
Function array
------------------------------------------------------------
-Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 76):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 71):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 78):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 78):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 85):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -26,7 +71,32 @@ Prove: (v[i]=true).
------------------------------------------------------------
-Goal Loop assigns 'CHECK':
+Goal Loop assigns (file assigned_initialized_memvar.i, line 72):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 79):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 75):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 75):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 82):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 82):
Prove: true.
------------------------------------------------------------
@@ -34,7 +104,38 @@ Prove: true.
Function comp
------------------------------------------------------------
-Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 131):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 133):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 133):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 140):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 140):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 148):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
@@ -54,7 +155,32 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
-Goal Loop assigns 'CHECK':
+Goal Loop assigns (file assigned_initialized_memvar.i, line 134):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 141):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 137):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 137):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 144):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 144):
Prove: true.
------------------------------------------------------------
@@ -62,7 +188,28 @@ Prove: true.
Function descr
------------------------------------------------------------
-Goal Preservation of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 105):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 112):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 112):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 119):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
@@ -71,13 +218,13 @@ Assume {
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i.
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (v[i_2]=true))).
- (* Loop assigns 'CHECK' *)
+ (* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\
(forall i_2 : Z. ((i_2 != 0) -> ((i_2 != 2) -> ((i_2 != 4) ->
((0 <= i_2) -> ((i_2 <= 9) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))))).
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: ((Init_s_1.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
((Init_s_1.Init_F1_S_a)[i_2]=true)))).
@@ -116,7 +263,7 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
-Goal Establishment of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 105):
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 119):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -132,18 +279,23 @@ Prove: (v[i]=true).
------------------------------------------------------------
-Goal Check 'CHECK' (file assigned_initialized_memvar.i, line 111):
+Goal Check (file assigned_initialized_memvar.i, line 126):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (1/5):
+Goal Loop assigns (file assigned_initialized_memvar.i, line 113):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (2/5):
-Effect at line 108
+Goal Loop assigns (file assigned_initialized_memvar.i, line 120) (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 120) (2/5):
+Effect at line 123
Assume {
Type: is_sint32(i_2) /\ is_sint32(i_3).
(* Goal *)
@@ -155,9 +307,9 @@ Assume {
(forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) -> (v[i_5]=true)))))).
(* Else *)
Have: 10 <= i_2.
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) -> (v[i_5]=true))).
- (* Loop assigns 'CHECK' *)
+ (* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\
(forall i_5 : Z. ((i_5 != 0) -> ((i_5 != 2) -> ((i_5 != 4) ->
((0 <= i_5) -> ((i_5 <= 9) -> ((s.F1_S_a)[i_5] = v_1[i_5]))))))).
@@ -177,20 +329,40 @@ Prove: ((i != 0) /\ (i != 2) /\ (i != 4)) \/
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (3/5):
-Effect at line 109
+Goal Loop assigns (file assigned_initialized_memvar.i, line 120) (3/5):
+Effect at line 124
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 120) (4/5):
+Effect at line 124
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 120) (5/5):
+Effect at line 124
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (4/5):
-Effect at line 109
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 116):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (5/5):
-Effect at line 109
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 116):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 123):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 123):
Prove: true.
------------------------------------------------------------
@@ -198,7 +370,28 @@ Prove: true.
Function field
------------------------------------------------------------
-Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 57):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 51):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 51):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 64):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
@@ -216,7 +409,32 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
-Goal Loop assigns 'CHECK':
+Goal Loop assigns (file assigned_initialized_memvar.i, line 52):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 58):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 55):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 55):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 61):
Prove: true.
------------------------------------------------------------
@@ -224,7 +442,28 @@ Prove: true.
Function index
------------------------------------------------------------
-Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 92):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 92):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 92):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file assigned_initialized_memvar.i, line 105):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
@@ -242,13 +481,38 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
+Goal Loop assigns (file assigned_initialized_memvar.i, line 93):
+Prove: true.
+
+------------------------------------------------------------
+
Goal Loop assigns 'CHECK' (1/2):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/2):
-Effect at line 90
+Effect at line 103
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 96):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 96):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 102):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 102):
Prove: true.
------------------------------------------------------------
@@ -256,10 +520,10 @@ Prove: true.
Function initialize
------------------------------------------------------------
-Goal Preservation of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 17):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 17):
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(((0 < i) ->
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
@@ -272,17 +536,17 @@ Prove: ((-1) <= i) /\
------------------------------------------------------------
-Goal Establishment of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 17):
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 17):
Prove: true.
------------------------------------------------------------
-Goal Check 'CHECK' (file assigned_initialized_memvar.i, line 22):
+Goal Check (file assigned_initialized_memvar.i, line 23):
Assume {
Have: 0 <= i.
Have: i <= 9.
Type: is_sint32(i_1).
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(((0 < i_1) ->
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
@@ -293,7 +557,17 @@ Prove: (v[i]=true).
------------------------------------------------------------
-Goal Loop assigns 'CHECK':
+Goal Loop assigns (file assigned_initialized_memvar.i, line 18):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 21):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 21):
Prove: true.
------------------------------------------------------------
@@ -301,7 +575,28 @@ Prove: true.
Function range
------------------------------------------------------------
-Goal Preservation of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 35):
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 30):
+Assume {
+ Type: is_sint32(i) /\ is_sint32(1 + i).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (v[i_1]=true)))))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: ((-1) <= i) /\
+ (forall i_1 : Z. ((i_1 <= i) -> ((0 <= i_1) ->
+ (v[i <- true][i_1]=true)))).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 30):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file assigned_initialized_memvar.i, line 37):
Let a = Init_s_0.Init_F1_S_a.
Assume {
Type: is_sint32(i_1) /\ is_sint32(i).
@@ -315,13 +610,13 @@ Assume {
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i_1.
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (v[i_2]=true))).
- (* Loop assigns 'CHECK' *)
+ (* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
(((i_2 <= 0) \/ (5 <= i_2)) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))).
- (* Invariant 'CHECK' *)
+ (* Invariant *)
Have: ((Init_s_0.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (a[i_2]=true)))).
(* Then *)
@@ -332,7 +627,7 @@ Prove: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
------------------------------------------------------------
-Goal Establishment of Invariant 'CHECK' (file assigned_initialized_memvar.i, line 35):
+Goal Establishment of Invariant (file assigned_initialized_memvar.i, line 37):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -348,18 +643,43 @@ Prove: (v[i]=true).
------------------------------------------------------------
-Goal Check 'CHECK' (file assigned_initialized_memvar.i, line 41):
+Goal Check (file assigned_initialized_memvar.i, line 44):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (1/2):
+Goal Loop assigns (file assigned_initialized_memvar.i, line 31):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'CHECK' (2/2):
-Effect at line 39
+Goal Loop assigns (file assigned_initialized_memvar.i, line 38) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file assigned_initialized_memvar.i, line 38) (2/2):
+Effect at line 42
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 34):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 34):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file assigned_initialized_memvar.i, line 41):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file assigned_initialized_memvar.i, line 41):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 587c090f8284138bd0a5aa71eb6be18c01c8ca00..b607053f0d6ff1766b92972857ab0b55bafc839a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -1,45 +1,104 @@
-# frama-c -wp -wp-timeout 20 [...]
+# frama-c -wp -wp-timeout 25 [...]
[kernel] Parsing assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
+[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] 26 goals scheduled
-[wp] [Valid] typed_initialize_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
-[wp] [Valid] typed_initialize_loop_invariant_CHECK_established (Qed)
-[wp] [Valid] typed_initialize_check_CHECK (Alt-Ergo) (Cached)
+[wp] [Valid] Goal comp_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal comp_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal descr_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal descr_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal field_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal field_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal index_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal index_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal initialize_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal initialize_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal range_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal range_terminates (Cfg) (Trivial)
+[wp] 70 goals scheduled
+[wp] [Valid] typed_initialize_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_initialize_loop_invariant_established (Qed)
+[wp] [Valid] typed_initialize_check (Alt-Ergo) (Cached)
[wp] [Valid] typed_initialize_loop_assigns (Qed)
-[wp] [Valid] typed_range_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
-[wp] [Valid] typed_range_loop_invariant_CHECK_established (Alt-Ergo) (Cached)
-[wp] [Valid] typed_range_check_CHECK (Qed)
-[wp] [Valid] typed_range_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_range_loop_assigns_part2 (Qed)
-[wp] [Unsuccess] typed_field_check_FAILS (Alt-Ergo) (Cached)
+[wp] [Valid] typed_initialize_loop_variant_decrease (Qed)
+[wp] [Valid] typed_initialize_loop_variant_positive (Qed)
+[wp] [Valid] typed_range_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_range_loop_invariant_established (Qed)
+[wp] [Valid] typed_range_loop_invariant_2_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_range_loop_invariant_2_established (Alt-Ergo) (Cached)
+[wp] [Valid] typed_range_check (Qed)
+[wp] [Valid] typed_range_loop_assigns (Qed)
+[wp] [Valid] typed_range_loop_assigns_2_part1 (Qed)
+[wp] [Valid] typed_range_loop_assigns_2_part2 (Qed)
+[wp] [Valid] typed_range_loop_variant_decrease (Qed)
+[wp] [Valid] typed_range_loop_variant_positive (Qed)
+[wp] [Valid] typed_range_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_range_loop_variant_2_positive (Qed)
+[wp] [Valid] typed_field_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_field_loop_invariant_established (Qed)
[wp] [Valid] typed_field_loop_assigns (Qed)
-[wp] [Unsuccess] typed_array_check_FAILS (Alt-Ergo) (Cached)
+[wp] [Valid] typed_field_loop_assigns_2 (Qed)
+[wp] [Valid] typed_field_loop_variant_decrease (Qed)
+[wp] [Valid] typed_field_loop_variant_positive (Qed)
+[wp] [Valid] typed_field_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_field_loop_variant_2_positive (Qed)
+[wp] [Valid] typed_array_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_array_loop_invariant_established (Qed)
+[wp] [Valid] typed_array_loop_invariant_2_preserved (Qed)
+[wp] [Valid] typed_array_loop_invariant_2_established (Qed)
[wp] [Valid] typed_array_loop_assigns (Qed)
-[wp] [Unsuccess] typed_index_check_FAILS (Alt-Ergo) (Cached)
-[wp] [Valid] typed_index_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_index_loop_assigns_part2 (Qed)
-[wp] [Valid] typed_descr_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
-[wp] [Valid] typed_descr_loop_invariant_CHECK_established (Alt-Ergo) (Cached)
-[wp] [Valid] typed_descr_check_CHECK (Qed)
-[wp] [Valid] typed_descr_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_descr_loop_assigns_part2 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_descr_loop_assigns_part3 (Qed)
-[wp] [Valid] typed_descr_loop_assigns_part4 (Qed)
-[wp] [Valid] typed_descr_loop_assigns_part5 (Qed)
-[wp] [Unsuccess] typed_comp_check_FAILS (Alt-Ergo) (Cached)
+[wp] [Valid] typed_array_loop_assigns_2 (Qed)
+[wp] [Valid] typed_array_loop_variant_decrease (Qed)
+[wp] [Valid] typed_array_loop_variant_positive (Qed)
+[wp] [Valid] typed_array_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_array_loop_variant_2_positive (Qed)
+[wp] [Valid] typed_index_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_index_loop_invariant_established (Qed)
+[wp] [Valid] typed_index_loop_assigns (Qed)
+[wp] [Valid] typed_index_loop_assigns_2_part1 (Qed)
+[wp] [Valid] typed_index_loop_assigns_2_part2 (Qed)
+[wp] [Valid] typed_index_loop_variant_decrease (Qed)
+[wp] [Valid] typed_index_loop_variant_positive (Qed)
+[wp] [Valid] typed_index_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_index_loop_variant_2_positive (Qed)
+[wp] [Valid] typed_descr_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_descr_loop_invariant_established (Qed)
+[wp] [Valid] typed_descr_loop_invariant_2_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_descr_loop_invariant_2_established (Alt-Ergo) (Cached)
+[wp] [Valid] typed_descr_check (Qed)
+[wp] [Valid] typed_descr_loop_assigns (Qed)
+[wp] [Valid] typed_descr_loop_assigns_2_part1 (Qed)
+[wp] [Valid] typed_descr_loop_assigns_2_part2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_descr_loop_assigns_2_part3 (Qed)
+[wp] [Valid] typed_descr_loop_assigns_2_part4 (Qed)
+[wp] [Valid] typed_descr_loop_assigns_2_part5 (Qed)
+[wp] [Valid] typed_descr_loop_variant_decrease (Qed)
+[wp] [Valid] typed_descr_loop_variant_positive (Qed)
+[wp] [Valid] typed_descr_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_descr_loop_variant_2_positive (Qed)
+[wp] [Valid] typed_comp_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_comp_loop_invariant_established (Qed)
+[wp] [Valid] typed_comp_loop_invariant_2_preserved (Qed)
+[wp] [Valid] typed_comp_loop_invariant_2_established (Qed)
[wp] [Valid] typed_comp_loop_assigns (Qed)
-[wp] Proved goals: 22 / 26
- Qed: 15
- Alt-Ergo: 7
- Unsuccess: 4
+[wp] [Valid] typed_comp_loop_assigns_2 (Qed)
+[wp] [Valid] typed_comp_loop_variant_decrease (Qed)
+[wp] [Valid] typed_comp_loop_variant_positive (Qed)
+[wp] [Valid] typed_comp_loop_variant_2_decrease (Qed)
+[wp] [Valid] typed_comp_loop_variant_2_positive (Qed)
+[wp] Proved goals: 84 / 84
+ Terminating: 7
+ Unreachable: 7
+ Qed: 57
+ Alt-Ergo: 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- initialize 2 2 4 100%
- range 3 2 5 100%
- field 1 - 2 50.0%
- array 1 - 2 50.0%
- index 2 - 3 66.7%
- descr 5 3 8 100%
- comp 1 - 2 50.0%
+ initialize 4 2 6 100%
+ range 9 3 12 100%
+ field 7 1 8 100%
+ array 9 1 10 100%
+ index 8 1 9 100%
+ descr 11 4 15 100%
+ comp 9 1 10 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index 78be993b741229582656eeb503231ec0c02c86fb..f6ff3c8b428bf1e8a94542f8884e7c1e3e4c4e71 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -35,22 +35,22 @@
[wp] [Unsuccess] typed_test_check_unknown_12 (Alt-Ergo) (Cached)
[wp] [Valid] typed_test_check_provable_3 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_test_check_unknown_13 (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_test_check_provable_4 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_test_check_provable_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_glob_var_ensures_provable (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_glob_var_ensures_unknown (Alt-Ergo) (Cached)
[wp] [Valid] typed_glob_arr_ensures_provable (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_glob_arr_ensures_unknown (Alt-Ergo) (Cached)
[wp] [Valid] typed_formal_assert_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_ptr_on_local_assert_provable (Alt-Ergo) (Cached)
-[wp] Proved goals: 23 / 39
+[wp] Proved goals: 24 / 39
Terminating: 5
Unreachable: 5
Qed: 6
- Alt-Ergo: 7
- Unsuccess: 16
+ Alt-Ergo: 8
+ Unsuccess: 15
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- test 6 3 23 39.1%
+ test 6 4 23 43.5%
glob_var - 1 2 50.0%
glob_arr - 1 2 50.0%
formal - 1 1 100%
diff --git a/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle b/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
index 7e926b602093199cfa7938976f0c8e502e675ed6..71c5f9d95e711ffc9e29f4b85daa8584aae10a38 100644
--- a/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
+++ b/src/plugins/wp/tests/wp_bytes/oracle_qualif/integers.res.oracle
@@ -44,7 +44,7 @@
[wp] [Valid] bytes_raw_signed_neg_check_7 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_signed_neg_check_8 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check (Alt-Ergo) (Cached)
-[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_2 (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_raw_cast_unsigned_signed_pos_check_2 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_3 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_unsigned_signed_pos_check_4 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_unsigned_signed_neg_check (Alt-Ergo) (Cached)
@@ -67,23 +67,24 @@
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_pos_check_7 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_2 (Alt-Ergo) (Cached)
-[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_3 (Alt-Ergo) (Cached)
+[wp] [Unsuccess] bytes_raw_cast_from_bytes_to_signed_neg_check_3 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_4 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_5 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_6 (Alt-Ergo) (Cached)
[wp] [Valid] bytes_raw_cast_from_bytes_to_signed_neg_check_7 (Alt-Ergo) (Cached)
-[wp] Proved goals: 69 / 69
+[wp] Proved goals: 67 / 69
Terminating: 8
Unreachable: 8
- Alt-Ergo: 53
+ Alt-Ergo: 51
+ Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
unsigned_ - 8 8 100%
signed_pos - 8 8 100%
signed_neg - 8 8 100%
- cast_unsigned_signed_pos - 4 4 100%
+ cast_unsigned_signed_pos - 3 4 75.0%
cast_unsigned_signed_neg - 4 4 100%
cast_from_bytes_to_unsigned - 7 7 100%
cast_from_bytes_to_signed_pos - 7 7 100%
- cast_from_bytes_to_signed_neg - 7 7 100%
+ cast_from_bytes_to_signed_neg - 6 7 85.7%
------------------------------------------------------------