diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index b71a4378c186dc59df8bc2eea6b1cddcbc28ad2c..25d3218843795c5157b54a1685279812b6263ce3 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -467,8 +467,8 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| tau ->
match List.find (fun spe -> spe.Lang.For_export.for_tau tau) !specific_equalities with
| spe when cnv.polarity = `Positive -> of_term ~cnv expected (spe.mk_new_eq a b)
- | exception Not_found -> Why3.Term.t_equ (of_term' cnv a) (of_term' cnv b)
- | _ -> Why3.Term.t_equ (of_term' cnv a) (of_term' cnv b)
+ | exception Not_found -> poly ~cnv Why3.Term.t_equ a b
+ | _ -> poly ~cnv Why3.Term.t_equ a b
end
| Neq (a,b), _, Prop ->
begin
@@ -479,13 +479,13 @@ let rec of_term ~cnv expected t : Why3.Term.term =
match List.find (fun spe -> spe.Lang.For_export.for_tau tau) !specific_equalities with
| spe when cnv.polarity = `Negative ->
Why3.Term.t_not (of_term ~cnv expected (spe.mk_new_eq a b))
- | exception Not_found -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
- | _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
+ | exception Not_found -> poly ~cnv Why3.Term.t_neq a b
+ | _ -> poly ~cnv Why3.Term.t_neq a b
end
| Eq (a,b), _, Bool ->
- t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
+ poly ~cnv (fun a b -> t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["eqb"] [a;b]) a b
| Neq (a,b), _, Bool ->
- t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
+ poly ~cnv (fun a b -> t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["neqb"] [a;b]) a b
| If(a,b,c), _, _ ->
let cnv' = {cnv with polarity = `NoPolarity} in
Why3.Term.t_if (of_term ~cnv:cnv' Prop a) (of_term ~cnv expected b) (of_term ~cnv expected c)
@@ -678,6 +678,15 @@ and int_or_real ~cnv ~fint ~lint ~pint ~freal ~lreal ~preal a b =
t_app_fold ~f:freal ~l:lreal ~p:preal ~cnv Real [a; b]
| _ -> assert false
+and poly ~cnv f a b =
+ match Lang.F.typeof a, Lang.F.typeof b with
+ | Int,Int ->
+ f (of_term ~cnv Int a) (of_term ~cnv Int b)
+ | Int,Real | Real,Int | Real,Real ->
+ f (of_term ~cnv Real a) (of_term ~cnv Real b)
+ | ta,tb ->
+ f (of_term ~cnv ta a) (of_term ~cnv tb b)
+
let rebuild cnv t =
let t, cache = Lang.For_export.rebuild ~cache:cnv.convert_for_export t in
cnv.convert_for_export <- cache;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
index fd91683d6c3534ddf9e63e1640bc8c4d3c871caa..9ba398399278b1469c599882ee1765879e2e6cf3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
@@ -4,6 +4,8 @@
[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal init_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal init_terminates (Cfg) (Trivial)
------------------------------------------------------------
Function foo
------------------------------------------------------------
@@ -12,3 +14,119 @@ Goal Assertion (file zero.i, line 14):
Prove: P_Foo(to_f64(.0)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function init
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file zero.i, line 24):
+Let a = shift_float64(s, 0).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (of_f64(havoc(Mf64_undef_0, Mf64_0, a, 10)[shift_float64(s, i_1)]) = .0))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file zero.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'is_zero' (file zero.i, line 25):
+Let x = to_uint32(1 + i).
+Let a = shift_float64(s, 0).
+Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < x).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (of_f64(a_1[shift_float64(s, i_2)]) = .0))).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant *)
+ Have: x <= 10.
+}
+Prove: of_f64(a_1[shift_float64(s, i) <- to_f64(.0)][shift_float64(s, i_1)])
+ = .0.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'is_zero' (file zero.i, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file zero.i, line 26) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file zero.i, line 26) (2/2):
+Effect at line 30
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file zero.i, line 19) in 'init' (1/2):
+Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file zero.i, line 19) in 'init' (2/2):
+Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file zero.i, line 29):
+Let x = to_uint32(1 + i).
+Let a = shift_float64(s, 0).
+Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (of_f64(a_1[shift_float64(s, i_1)]) = .0))).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant *)
+ Have: x <= 10.
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < x) ->
+ (of_f64(a_1[shift_float64(s, i) <- to_f64(.0)][shift_float64(s, i_1)])
+ = .0))).
+}
+Prove: i < x.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file zero.i, line 29):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
index 7107e0ff7ef3f3bb81e0bc28273bf2d1373d1cf8..8d825e0428891547822d7de7e0d66b6800a6d445 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
@@ -4,6 +4,8 @@
[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal init_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal init_terminates (Cfg) (Trivial)
------------------------------------------------------------
Function foo
------------------------------------------------------------
@@ -12,3 +14,117 @@ Goal Assertion (file zero.i, line 14):
Prove: P_Foo(.0).
------------------------------------------------------------
+------------------------------------------------------------
+ Function init
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file zero.i, line 24):
+Let a = shift_float64(s, 0).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (havoc(Mf64_undef_0, Mf64_0, a, 10)[shift_float64(s, i_1)] = 0))).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file zero.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'is_zero' (file zero.i, line 25):
+Let x = to_uint32(1 + i).
+Let a = shift_float64(s, 0).
+Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < x).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_1[shift_float64(s, i_2)] = 0))).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant *)
+ Have: x <= 10.
+}
+Prove: a_1[shift_float64(s, i) <- .0][shift_float64(s, i_1)] = 0.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'is_zero' (file zero.i, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file zero.i, line 26) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file zero.i, line 26) (2/2):
+Effect at line 30
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file zero.i, line 19) in 'init' (1/2):
+Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file zero.i, line 19) in 'init' (2/2):
+Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file zero.i, line 29):
+Let x = to_uint32(1 + i).
+Let a = shift_float64(s, 0).
+Let a_1 = havoc(Mf64_undef_0, Mf64_0, a, 10).
+Assume {
+ Type: is_uint32(i).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, a, 10).
+ (* Invariant *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (a_1[shift_float64(s, i_1)] = 0))).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant *)
+ Have: x <= 10.
+ (* Invariant 'is_zero' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < x) ->
+ (a_1[shift_float64(s, i) <- .0][shift_float64(s, i_1)] = 0))).
+}
+Prove: i < x.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file zero.i, line 29):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle
index e57f8818165526a100bb4ca6a3ce3f402df60cca..cb12515eb8ce31a2c5d7d25a4850db54e2aa7ddd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle
@@ -4,13 +4,27 @@
[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
+[wp] [Valid] Goal init_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal init_terminates (Cfg) (Trivial)
+[wp] 11 goals scheduled
[wp] [Valid] typed_foo_assert (Alt-Ergo) (Cached)
-[wp] Proved goals: 3 / 3
- Terminating: 1
- Unreachable: 1
- Alt-Ergo: 1
+[wp] [Valid] typed_init_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_init_loop_invariant_established (Qed)
+[wp] [Valid] typed_init_loop_invariant_is_zero_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_init_loop_invariant_is_zero_established (Qed)
+[wp] [Valid] typed_init_loop_assigns_part1 (Qed)
+[wp] [Valid] typed_init_loop_assigns_part2 (Qed)
+[wp] [Valid] typed_init_assigns_part1 (Qed)
+[wp] [Valid] typed_init_assigns_part2 (Qed)
+[wp] [Valid] typed_init_loop_variant_decrease (Alt-Ergo) (Cached)
+[wp] [Valid] typed_init_loop_variant_positive (Qed)
+[wp] Proved goals: 15 / 15
+ Terminating: 2
+ Unreachable: 2
+ Qed: 7
+ Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - 1 1 100%
+ init 7 3 10 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle
index 56784023dbc831bd8e74d867653e5c143c9dc4fa..1dbe562be60845d2bcb74fd6522ce9a57a29b08d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle
@@ -4,13 +4,27 @@
[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
+[wp] [Valid] Goal init_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal init_terminates (Cfg) (Trivial)
+[wp] 11 goals scheduled
[wp] [Valid] typed_real_foo_assert (Alt-Ergo) (Trivial)
-[wp] Proved goals: 3 / 3
- Terminating: 1
- Unreachable: 1
- Alt-Ergo: 1
+[wp] [Valid] typed_real_init_loop_invariant_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_real_init_loop_invariant_established (Qed)
+[wp] [Valid] typed_real_init_loop_invariant_is_zero_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_real_init_loop_invariant_is_zero_established (Qed)
+[wp] [Valid] typed_real_init_loop_assigns_part1 (Qed)
+[wp] [Valid] typed_real_init_loop_assigns_part2 (Qed)
+[wp] [Valid] typed_real_init_assigns_part1 (Qed)
+[wp] [Valid] typed_real_init_assigns_part2 (Qed)
+[wp] [Valid] typed_real_init_loop_variant_decrease (Alt-Ergo) (Cached)
+[wp] [Valid] typed_real_init_loop_variant_positive (Qed)
+[wp] Proved goals: 15 / 15
+ Terminating: 2
+ Unreachable: 2
+ Qed: 7
+ Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - 1 1 100%
+ init 7 3 10 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/zero.i b/src/plugins/wp/tests/wp_acsl/zero.i
index 20b69a4ac870e1996a6ced3372f04e996308648d..c9f43e9ccc85359bc82d30aa22ef757e7c25ab51 100644
--- a/src/plugins/wp/tests/wp_acsl/zero.i
+++ b/src/plugins/wp/tests/wp_acsl/zero.i
@@ -13,3 +13,20 @@
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
}
+
+/*@
+ requires \valid(s+(0..9));
+ assigns s[0..9];
+*/
+void init(double *s) {
+ unsigned int i;
+ /*@
+ loop invariant 0 <= i <= 10;
+ loop invariant is_zero: \forall integer k; 0 <= k < i ==> s[k] == 0;
+ loop assigns i, s[0..9];
+ loop variant 10-i;
+ */
+ for(i=0; i < 10; i++) {
+ s[i] = 0;
+ }
+}