diff --git a/src/libraries/qed/term.ml b/src/libraries/qed/term.ml
index e38cd36fa36a39fff9b72bb0409a96631a4179d7..a658843b9430b5fcc7310144b252ae0a00a6bacd 100644
--- a/src/libraries/qed/term.ml
+++ b/src/libraries/qed/term.ml
@@ -829,6 +829,8 @@ struct
let e_true = constant (insert True)
let e_zero = constant (insert (Kint Z.zero))
let e_one = constant (insert (Kint Z.one))
+ let e_zero_r = constant (insert (Kreal Q.zero))
+ let e_one_r = constant (insert (Kreal Q.one))
let e_int n = insert (Kint (Z.of_int n))
let e_float r = insert (Kreal (Q.of_float r))
let e_zint z = insert (Kint z)
@@ -852,16 +854,34 @@ struct
let c_fun f xs tau = insert ?tau (Fun(f,xs))
- let c_add = function
+ let c_add0 = function
+ | [] -> assert false
+ | xs -> insert(Add(List.sort compare xs))
+
+ let i_add = function
| [] -> e_zero
| [x] -> x
| xs -> insert(Add(List.sort compare xs))
- let c_mul = function
+ let r_add = function
+ | [] -> e_zero_r
+ | [x] -> x
+ | xs -> insert(Add(List.sort compare xs))
+
+ let c_mul0 = function
+ | [] -> assert false
+ | xs -> insert(Mul(List.sort compare xs))
+
+ let i_mul = function
| [] -> e_one
| [x] -> x
| xs -> insert(Mul(List.sort compare xs))
+ let r_mul = function
+ | [] -> e_one_r
+ | [x] -> x
+ | xs -> insert(Mul(List.sort compare xs))
+
let c_times z t = insert(Times(z,t))
let c_and = function
@@ -911,9 +931,8 @@ struct
with Exit ->
insert(Rdef (List.sort compare_field fxs))
- [@@@ warning "-32"]
let insert _ = assert false (* [insert] should not be used afterwards *)
- [@@@ warning "+32"]
+ [@@ warning "-32"]
let is_primitive e =
match e.repr with
@@ -1209,7 +1228,7 @@ struct
let rec times z e =
if Z.equal z Z.one then e else
- if Z.equal z Z.zero then e_zint Z.zero else
+ if Z.equal z Z.zero then if is_real e then e_zero_r else e_zero else
match e.repr with
| Kint z' -> e_zint (Z.mul z z')
| Kreal r -> e_real (q_times z r)
@@ -1226,27 +1245,27 @@ struct
let c = Q.sub a b in
match xs , ys with
| [] , [] -> if fz c Q.zero then e_true else e_false
- | [] , _ -> fe (e_real c) (c_add ys)
- | _ , [] -> fe (c_add xs) (e_real (Q.neg c))
+ | [] , _ -> fe (e_real c) (r_add ys)
+ | _ , [] -> fe (r_add xs) (e_real (Q.neg c))
| _ ->
let s = Q.sign c in
- if s < 0 then fe (c_add xs) (c_add (e_real (Q.neg c) :: ys)) else
- if s > 0 then fe (c_add (e_real c :: xs)) (c_add ys) else
- fe (c_add xs) (c_add ys)
+ if s < 0 then fe (r_add xs) (r_add (e_real (Q.neg c) :: ys)) else
+ if s > 0 then fe (r_add (e_real c :: xs)) (r_add ys) else
+ fe (r_add xs) (r_add ys)
let i_affine_rel fc fe c xs ys =
match xs , ys with
| [] , [] -> if fc c Z.zero then e_true else e_false
- | [] , _ -> fe (e_zint c) (c_add ys) (* c+0 R ys <-> c R ys *)
- | _ , [] -> fe (c_add xs) (e_zint (Z.neg c)) (* c+xs R 0 <-> xs R -c *)
+ | [] , _ -> fe (e_zint c) (i_add ys) (* c+0 R ys <-> c R ys *)
+ | _ , [] -> fe (i_add xs) (e_zint (Z.neg c)) (* c+xs R 0 <-> xs R -c *)
| _ ->
match sign c with
(* 0+xs R ys <-> xs R ys *)
- | Null -> fe (c_add xs) (c_add ys)
+ | Null -> fe (i_add xs) (i_add ys)
(* c+xs R ys <-> xs R (-c+ys) *)
- | Negative -> fe (c_add xs) (c_add (e_zint (Z.neg c) :: ys))
+ | Negative -> fe (i_add xs) (i_add (e_zint (Z.neg c) :: ys))
(* c+xs R ys <-> (c+xs) R ys *)
- | Positive -> fe (c_add (e_zint c :: xs)) (c_add ys)
+ | Positive -> fe (i_add (e_zint c :: xs)) (i_add ys)
let i_affine_leq c xs ys =
if Z.equal c Z.one
@@ -1371,26 +1390,26 @@ struct
(* --- Affine Dispatch --- *)
- let is_affine xs ys =
+ let is_affine_int xs ys =
not (List.exists is_real xs || List.exists is_real ys)
let affine_eq c xs ys =
- if is_affine xs ys
+ if is_affine_int xs ys
then i_affine_rel Z.equal c_builtin_eq c xs ys
else r_affine_rel Q.equal c_builtin_eq c xs ys
let affine_neq c xs ys =
- if is_affine xs ys
+ if is_affine_int xs ys
then i_affine_rel (fun x y -> not (Z.equal x y)) c_builtin_neq c xs ys
else r_affine_rel (fun x y -> not (Q.equal x y)) c_builtin_neq c xs ys
let affine_leq c xs ys =
- if is_affine xs ys
+ if is_affine_int xs ys
then i_affine_ratio_leq c xs ys
else r_affine_rel Q.leq c_builtin_leq c xs ys
let affine_lt c xs ys =
- if is_affine xs ys
+ if is_affine_int xs ys
then i_affine_ratio_lt c xs ys
else r_affine_rel Q.lt c_builtin_lt c xs ys
@@ -1450,14 +1469,16 @@ struct
let addition ts =
let kts = unfold_affine [] Z.one ts in
let kts = List.sort compare_monoms kts in
- c_add (fold_affine fold_monom [] kts)
+ let kts = fold_affine fold_monom [] kts in
+ if List.exists is_real ts then r_add kts else i_add kts
(* a and b normalized *)
let substraction a b =
let kts = unfold_affine1 [] Z.one a in
let kts = unfold_affine1 kts Z.minus_one b in
let kts = List.sort compare_monoms kts in
- c_add (fold_affine fold_monom [] kts)
+ let kts = fold_affine fold_monom [] kts in
+ if is_real a || is_real b then r_add kts else i_add kts
(* --- Relations --- *)
@@ -1543,20 +1564,23 @@ struct
let r,ts = r_ground Q.mul Q.one [] ts in
if Q.equal Q.zero r then e_real Q.zero else
if ts=[] then e_real r else
- if Q.equal r Q.one then c_mul ts else c_mul (e_real r :: ts)
+ if Q.equal r Q.one then r_mul ts else r_mul (e_real r :: ts)
else
let s,ts = i_ground Z.mul Z.one [] ts in
if Z.equal Z.zero s then e_zint Z.zero else
if ts=[] then e_zint s else
- let t = c_mul ts in
+ let t = i_mul ts in
if Z.equal s Z.one then t else c_times s t
let e_times k x =
if Z.equal k Z.one then x else
- if Z.equal k Z.zero then e_zero else
+ if Z.equal k Z.zero then
+ if is_real x then e_zero_r else e_zero
+ else
let kts = unfold_affine1 [] k x in
let kts = List.sort compare_monoms kts in
- c_add (fold_affine fold_monom [] kts)
+ let kts = fold_affine fold_monom [] kts in
+ if is_real x then r_add kts else i_add kts
(* --- Divisions --- *)
@@ -2141,8 +2165,8 @@ struct
match e0.repr with
| Kint _ | Kreal _ | Fvar _ | Bvar _ | True | False -> e0
| Not e -> c_not (f e)
- | Add xs -> c_add (List.map f xs)
- | Mul xs -> c_mul (List.map f xs)
+ | Add xs -> c_add0 (List.map f xs)
+ | Mul xs -> c_mul0 (List.map f xs)
| And xs -> c_and (List.map f xs)
| Or xs -> c_or (List.map f xs)
| Mod(x,y) -> c_mod (f x) (f y)
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
new file mode 100644
index 0000000000000000000000000000000000000000..9ba398399278b1469c599882ee1765879e2e6cf3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
@@ -0,0 +1,132 @@
+# frama-c -wp [...]
+[kernel] Parsing zero.i (no preprocessing)
+[wp] Running WP plugin...
+[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
+------------------------------------------------------------
+
+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
new file mode 100644
index 0000000000000000000000000000000000000000..8d825e0428891547822d7de7e0d66b6800a6d445
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
@@ -0,0 +1,130 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing zero.i (no preprocessing)
+[wp] Running WP plugin...
+[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
+------------------------------------------------------------
+
+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
new file mode 100644
index 0000000000000000000000000000000000000000..cb12515eb8ce31a2c5d7d25a4850db54e2aa7ddd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle
@@ -0,0 +1,30 @@
+# frama-c -wp [...]
+[kernel] Parsing zero.i (no preprocessing)
+[wp] Running WP plugin...
+[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)
+[wp] 11 goals scheduled
+[wp] [Valid] typed_foo_assert (Alt-Ergo) (Cached)
+[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
new file mode 100644
index 0000000000000000000000000000000000000000..1dbe562be60845d2bcb74fd6522ce9a57a29b08d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle
@@ -0,0 +1,30 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing zero.i (no preprocessing)
+[wp] Running WP plugin...
+[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)
+[wp] 11 goals scheduled
+[wp] [Valid] typed_real_foo_assert (Alt-Ergo) (Trivial)
+[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
new file mode 100644
index 0000000000000000000000000000000000000000..c9f43e9ccc85359bc82d30aa22ef757e7c25ab51
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/zero.i
@@ -0,0 +1,32 @@
+/* run.config
+ OPT:
+ OPT: -wp-model real
+*/
+
+/* run.config_qualif
+ OPT:
+ OPT: -wp-model real
+*/
+
+//@ predicate Foo(double y) = y == 0.0;
+
+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;
+ }
+}