From e21978b08c802ff24d7f0530da0e9e1da7eb62aa Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 10 Sep 2024 07:42:34 +0200
Subject: [PATCH] [wp] makes -wp-gen tests more deterministic
---
src/plugins/wp/tests/test_config | 2 +-
.../tests/wp_acsl/oracle/boolean.res.oracle | 4 +-
.../oracle/chunk_typing_usable.res.oracle | 132 ++++++++--------
.../wp_acsl/oracle/float_const.res.oracle | 24 +--
.../tests/wp_acsl/oracle/inductive.res.oracle | 130 ++++++++--------
.../wp_acsl/oracle/struct_fields.res.oracle | 54 +++----
.../tests/wp_acsl/oracle/sum_types.res.oracle | 94 +++++------
.../wp_plugin/oracle/float_driver.res.oracle | 146 +++++++++---------
.../wp_plugin/oracle/inductive.res.oracle | 82 +++++-----
9 files changed, 334 insertions(+), 334 deletions(-)
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index 9a3cee925ad..96a7134a641 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -2,5 +2,5 @@ PLUGIN: wp
MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
COMMENT: no need of "-wp-share" in Dune -> Dune finds it automatically
-CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
+CMD: @frama-c@ -wp -wp-par 1 -wp-prover none -wp-print -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
OPT:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
index fae672fa5ad..09b986c02e1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -5,9 +5,9 @@
[wp] [Valid] Goal u8_is_continue_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Generated] Goal typed_u8_is_continue_assigns_part3 (Qed)
-[wp] [Generated] Goal typed_u8_is_continue_assigns_part2 (Qed)
[wp] [Generated] Goal typed_u8_is_continue_assigns_part1 (Qed)
+[wp] [Generated] Goal typed_u8_is_continue_assigns_part2 (Qed)
+[wp] [Generated] Goal typed_u8_is_continue_assigns_part3 (Qed)
[wp] 4 goals generated
------------------------------------------------------------
Function u8_is_continue
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index 6d06e269bfd..012438ee56a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -9,7 +9,7 @@
[wp] [Valid] Goal usable_lemma_terminates (Cfg) (Trivial)
[wp] 3 goals scheduled
---------------------------------------------
---- Context 'typed_usable_lemma' Cluster 'Chunk'
+--- Context 'typed' Cluster 'Chunk'
---------------------------------------------
theory Chunk
@@ -36,7 +36,7 @@ theory Chunk
end
---------------------------------------------
---- Context 'typed_usable_lemma' Cluster 'Compound'
+--- Context 'typed' Cluster 'Compound'
---------------------------------------------
theory Compound
@@ -60,7 +60,7 @@ theory Compound
end
---------------------------------------------
---- Context 'typed_usable_lemma' Cluster 'A_Occ'
+--- Context 'typed' Cluster 'A_Occ'
---------------------------------------------
theory A_Occ
@@ -109,40 +109,6 @@ theory A_Occ
is_sint32_chunk mint ->
is_sint32 v -> is_sint32 x1 -> L_occ mint v p f x = L_occ mint v p f t
-end
----------------------------------------------
---- Context 'typed_usable_lemma' Cluster 'Axiomatic1'
----------------------------------------------
-theory Axiomatic1
-
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use frama_c_wp.memaddr.MemAddr *)
-
- (* use Chunk *)
-
- (* use A_Occ *)
-
- lemma Q_provable_lemma :
- forall mint:addr -> int, v:int, p:addr, f:int, s:int, t:int.
- f <= s ->
- s <= t ->
- is_sint32_chunk mint ->
- is_sint32 v ->
- (L_occ mint v p f s + L_occ mint v p s t) = L_occ mint v p f t
-
end
[wp:print-generated]
theory WP
@@ -161,19 +127,19 @@ end
(* use map.Map *)
- (* use Axiomatic1 *)
+ (* use frama_c_wp.memaddr.MemAddr *)
+
+ (* use Chunk *)
+
+ (* use A_Occ *)
goal wp_goal :
- forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
- i3 <= i1 ->
- i < i3 ->
- region (a.base) <= 0 ->
+ forall t:addr -> int, i:int, a:addr, i1:int, i2:int, i3:int.
+ i1 <= i2 ->
+ i <= i1 ->
is_sint32_chunk t ->
- is_uint32 i3 ->
- is_uint32 i1 ->
- is_uint32 i ->
- is_sint32 i2 ->
- (L_occ t i2 a i i3 + L_occ t i2 a i3 i1) = L_occ t i2 a i i1
+ is_sint32 i3 ->
+ (L_occ t i3 a i i1 + L_occ t i3 a i1 i2) = L_occ t i3 a i i2
end
---------------------------------------------
@@ -283,7 +249,7 @@ end
---------------------------------------------
--- Context 'typed_usable_axiom' Cluster 'Axiomatic1'
---------------------------------------------
-theory Axiomatic11
+theory Axiomatic1
(* use why3.BuiltIn.BuiltIn *)
@@ -305,7 +271,7 @@ theory Axiomatic11
(* use A_Occ1 *)
- lemma Q_provable_lemma1 :
+ lemma Q_provable_lemma :
forall mint:addr1 -> int, v:int, p:addr1, f:int, s:int, t:int.
f <=' s ->
s <=' t ->
@@ -331,22 +297,22 @@ end
(* use map.Map1 *)
- (* use Axiomatic11 *)
+ (* use Axiomatic1 *)
goal wp_goal :
forall t:addr1 -> int, a:addr1, i:int, i1:int, i2:int.
let x = (- 1) +' i1 in
not get1 t (shift_sint321 a x) = i2 ->
i <' i1 ->
- region1 (a.base1) <=' 0 ->
+ region (a.base) <=' 0 ->
i1 <=' 1000 ->
is_sint32_chunk1 t ->
- is_uint321 i1 ->
- is_uint321 i -> is_sint321 i2 -> L_occ1 t i2 a i x = L_occ1 t i2 a i i1
+ is_uint32 i1 ->
+ is_uint32 i -> is_sint321 i2 -> L_occ1 t i2 a i x = L_occ1 t i2 a i i1
end
---------------------------------------------
---- Context 'typed' Cluster 'Chunk'
+--- Context 'typed_usable_lemma' Cluster 'Chunk'
---------------------------------------------
theory Chunk2
@@ -373,7 +339,7 @@ theory Chunk2
end
---------------------------------------------
---- Context 'typed' Cluster 'Compound'
+--- Context 'typed_usable_lemma' Cluster 'Compound'
---------------------------------------------
theory Compound2
@@ -397,7 +363,7 @@ theory Compound2
end
---------------------------------------------
---- Context 'typed' Cluster 'A_Occ'
+--- Context 'typed_usable_lemma' Cluster 'A_Occ'
---------------------------------------------
theory A_Occ2
@@ -448,6 +414,40 @@ theory A_Occ2
is_sint322 v ->
is_sint322 x1 -> L_occ2 mint v p f x = L_occ2 mint v p f t
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'Axiomatic1'
+---------------------------------------------
+theory Axiomatic11
+
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool2 *)
+
+ (* use int.Int2 *)
+
+ (* use int.ComputerDivision2 *)
+
+ (* use real.RealInfix2 *)
+
+ (* use frama_c_wp.qed.Qed2 *)
+
+ (* use map.Map2 *)
+
+ (* use frama_c_wp.memaddr.MemAddr2 *)
+
+ (* use Chunk2 *)
+
+ (* use A_Occ2 *)
+
+ lemma Q_provable_lemma1 :
+ forall mint:addr2 -> int, v:int, p:addr2, f:int, s:int, t:int.
+ f <='' s ->
+ s <='' t ->
+ is_sint32_chunk2 mint ->
+ is_sint322 v ->
+ (L_occ2 mint v p f s +'' L_occ2 mint v p s t) = L_occ2 mint v p f t
+
end
[wp:print-generated]
theory WP2
@@ -466,19 +466,19 @@ end
(* use map.Map2 *)
- (* use frama_c_wp.memaddr.MemAddr2 *)
-
- (* use Chunk2 *)
-
- (* use A_Occ2 *)
+ (* use Axiomatic11 *)
goal wp_goal :
- forall t:addr2 -> int, i:int, a:addr2, i1:int, i2:int, i3:int.
- i1 <='' i2 ->
- i <='' i1 ->
+ forall t:addr2 -> int, a:addr2, i:int, i1:int, i2:int, i3:int.
+ i3 <='' i1 ->
+ i <'' i3 ->
+ region1 (a.base1) <='' 0 ->
is_sint32_chunk2 t ->
- is_sint322 i3 ->
- (L_occ2 t i3 a i i1 +'' L_occ2 t i3 a i1 i2) = L_occ2 t i3 a i i2
+ is_uint321 i3 ->
+ is_uint321 i1 ->
+ is_uint321 i ->
+ is_sint322 i2 ->
+ (L_occ2 t i2 a i i3 +'' L_occ2 t i2 a i3 i1) = L_occ2 t i2 a i i1
end
[wp] 3 goals generated
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
index 0a48f57995b..1416c4c4fce 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
@@ -39,9 +39,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t.
- let r = of_f32 f in
- eq_f32 f (0x1.99999Ap-4:t) -> of_f32 (to_f32 (of_f64 (to_f64 r))) = r
+ forall f:t. eq_f32 f (0x1.99999Ap-4:t) -> not of_f32 f = (1.0 / 10.0)
end
[wp:print-generated]
@@ -73,8 +71,7 @@
goal wp_goal :
forall f:t.
- eq_f32 f (0x1.99999Ap-4:t) ->
- not of_f32 f = (3602879701896397.0 / 36028797018963968.0)
+ eq_f32 f (0x1.99999Ap-4:t) -> of_f32 f = (13421773.0 / 134217728.0)
end
[wp:print-generated]
@@ -106,7 +103,8 @@
goal wp_goal :
forall f:t.
- eq_f32 f (0x1.99999Ap-4:t) -> of_f32 f = (13421773.0 / 134217728.0)
+ eq_f32 f (0x1.99999Ap-4:t) ->
+ not of_f32 f = (3602879701896397.0 / 36028797018963968.0)
end
[wp:print-generated]
@@ -137,7 +135,9 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t. eq_f32 f (0x1.99999Ap-4:t) -> not of_f32 f = (1.0 / 10.0)
+ forall f:t.
+ let r = of_f32 f in
+ eq_f32 f (0x1.99999Ap-4:t) -> of_f32 (to_f32 (of_f64 (to_f64 r))) = r
end
[wp:print-generated]
@@ -169,8 +169,7 @@
goal wp_goal :
forall f:t1.
- let r = of_f321 (to_f321 (of_f641 f)) in
- eq_f64 f (0x1.999999999999Ap-4:t1) -> of_f641 (to_f641 r) = r
+ eq_f64 f (0x1.999999999999Ap-4:t1) -> not of_f641 f = (1.0 /' 10.0)
end
[wp:print-generated]
@@ -203,7 +202,7 @@
goal wp_goal :
forall f:t1.
eq_f64 f (0x1.999999999999Ap-4:t1) ->
- not of_f641 f = (13421773.0 /' 134217728.0)
+ of_f641 f = (3602879701896397.0 /' 36028797018963968.0)
end
[wp:print-generated]
@@ -236,7 +235,7 @@
goal wp_goal :
forall f:t1.
eq_f64 f (0x1.999999999999Ap-4:t1) ->
- of_f641 f = (3602879701896397.0 /' 36028797018963968.0)
+ not of_f641 f = (13421773.0 /' 134217728.0)
end
[wp:print-generated]
@@ -268,7 +267,8 @@
goal wp_goal :
forall f:t1.
- eq_f64 f (0x1.999999999999Ap-4:t1) -> not of_f641 f = (1.0 /' 10.0)
+ let r = of_f321 (to_f321 (of_f641 f)) in
+ eq_f64 f (0x1.999999999999Ap-4:t1) -> of_f641 (to_f641 r) = r
end
[wp] 8 goals generated
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 924d87a09bb..11d4b9d4681 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -45,14 +45,6 @@ end
(* use map.Map *)
- inductive P_is_gcd int int int =
- | Q_gcd_zero : forall n:int. P_is_gcd n 0 n
- | Q_gcd_succ :
- forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
-
- lemma Q_test_no_label :
- forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
-
(* use frama_c_wp.memaddr.MemAddr *)
(* use Compound *)
@@ -67,9 +59,61 @@ end
P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root))
node -> P_reachable malloc mptr root node
+ lemma Q_test_one_label :
+ forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
+ addr -> addr, l1:addr, l2:addr.
+ P_reachable malloc1 mptr1 l1 l2 -> not P_reachable malloc mptr l1 l2
+
+ inductive P_is_gcd int int int =
+ | Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+ | Q_gcd_succ :
+ forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+
+ lemma Q_test_no_label :
+ forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
+
+ predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
+ addr) (begin1:int) (end1:int) =
+ forall i:int.
+ begin1 <= i ->
+ i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
+
+ predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
+ (begin1:int) (i:int) (j:int) (end1:int) =
+ ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
+ get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
+ begin1 <= i) /\
+ i < j) /\
+ j < end1) /\
+ (forall i1:int.
+ not i1 = i ->
+ not j = i1 ->
+ begin1 <= i1 ->
+ i1 < end1 ->
+ get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
+
+ inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
+ | Q_refl :
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
+ int, end1:int.
+ P_same_array mint mint1 a b begin1 end1 ->
+ P_same_elements mint mint1 a b begin1 end1
+ | Q_swap :
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
+ int, i:int, j:int, end1:int.
+ P_swap mint mint1 a b begin1 i j end1 ->
+ P_same_elements mint mint1 a b begin1 end1
+ | Q_trans :
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
+ addr, b:addr, c:addr, begin1:int, end1:int.
+ P_same_elements mint mint1 b c begin1 end1 ->
+ P_same_elements mint1 mint2 a b begin1 end1 ->
+ P_same_elements mint mint2 a c begin1 end1
+
goal wp_goal :
- forall t:int -> int, t1:int -> int, t2:addr -> addr, t3:addr -> addr, a:
- addr, a1:addr. P_reachable t1 t3 a a1 -> not P_reachable t t2 a a1
+ forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
+ int, i1:int, i2:int, i3:int.
+ P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
end
[wp:print-generated]
@@ -116,6 +160,15 @@ end
(* use map.Map *)
+ inductive P_is_gcd2 int int int =
+ | Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+ | Q_gcd_succ2 :
+ forall a:int, b:int, d:int.
+ P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+
+ lemma Q_test_no_label1 :
+ forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
+
(* use frama_c_wp.memaddr.MemAddr *)
(* use Compound *)
@@ -130,62 +183,9 @@ end
P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root))
node -> P_reachable1 malloc mptr root node
- lemma Q_test_one_label :
- forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
- addr -> addr, l1:addr, l2:addr.
- P_reachable1 malloc1 mptr1 l1 l2 -> not P_reachable1 malloc mptr l1 l2
-
- inductive P_is_gcd2 int int int =
- | Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
- | Q_gcd_succ2 :
- forall a:int, b:int, d:int.
- P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
-
- lemma Q_test_no_label1 :
- forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
-
- predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin1:int) (end1:int) =
- forall i:int.
- begin1 <= i ->
- i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
-
- predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin1:int) (i:int) (j:int) (end1:int) =
- ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
- get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin1 <= i) /\
- i < j) /\
- j < end1) /\
- (forall i1:int.
- not i1 = i ->
- not j = i1 ->
- begin1 <= i1 ->
- i1 < end1 ->
- get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
-
- inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
- | Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
- int, end1:int.
- P_same_array mint mint1 a b begin1 end1 ->
- P_same_elements mint mint1 a b begin1 end1
- | Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
- int, i:int, j:int, end1:int.
- P_swap mint mint1 a b begin1 i j end1 ->
- P_same_elements mint mint1 a b begin1 end1
- | Q_trans :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
- addr, b:addr, c:addr, begin1:int, end1:int.
- P_same_elements mint mint1 b c begin1 end1 ->
- P_same_elements mint1 mint2 a b begin1 end1 ->
- P_same_elements mint mint2 a c begin1 end1
-
goal wp_goal :
- forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
- int, i1:int, i2:int, i3:int.
- P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
+ forall t:int -> int, t1:int -> int, t2:addr -> addr, t3:addr -> addr, a:
+ addr, a1:addr. P_reachable1 t1 t3 a a1 -> not P_reachable1 t t2 a a1
end
[wp] 3 goals generated
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 50896287c81..f43f3e075ee 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -6,9 +6,9 @@
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] 2 goals scheduled
---------------------------------------------
---- Context 'typed_foo' Cluster 'Chunk'
+--- Context 'typed_foo' Cluster 'S1_X'
---------------------------------------------
-theory Chunk
+theory S1_X
(* use why3.BuiltIn.BuiltIn *)
@@ -24,24 +24,19 @@ theory Chunk
(* use map.Map *)
- (* use frama_c_wp.memaddr.MemAddr *)
+ type S1_X =
+ | S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
(* use frama_c_wp.cint.Cint *)
- predicate is_sint8_chunk (m:addr -> int) =
- forall a:addr. is_sint8 (get m a)
-
- predicate is_sint16_chunk (m:addr -> int) =
- forall a:addr. is_sint16 (get m a)
-
- predicate is_sint32_chunk (m:addr -> int) =
- forall a:addr. is_sint32 (get m a)
+ predicate IsS1_X (s:S1_X) =
+ (is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
end
---------------------------------------------
---- Context 'typed_foo' Cluster 'S1_X'
+--- Context 'typed_foo' Cluster 'Chunk'
---------------------------------------------
-theory S1_X
+theory Chunk
(* use why3.BuiltIn.BuiltIn *)
@@ -57,13 +52,18 @@ theory S1_X
(* use map.Map *)
- type S1_X =
- | S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
+ (* use frama_c_wp.memaddr.MemAddr *)
(* use frama_c_wp.cint.Cint *)
- predicate IsS1_X (s:S1_X) =
- (is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
+ predicate is_sint8_chunk (m:addr -> int) =
+ forall a:addr. is_sint8 (get m a)
+
+ predicate is_sint16_chunk (m:addr -> int) =
+ forall a:addr. is_sint16 (get m a)
+
+ predicate is_sint32_chunk (m:addr -> int) =
+ forall a:addr. is_sint32 (get m a)
end
---------------------------------------------
@@ -239,25 +239,25 @@ end
(* use frama_c_wp.memaddr.MemAddr *)
+ (* use S1_X *)
+
(* use Chunk *)
(* use frama_c_wp.memory.Memory *)
- (* use S1_X *)
-
(* use Compound *)
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
- addr -> int, a:addr.
+ addr -> int, a:addr, x:S1_X.
region (a.base) <= 0 ->
+ IsS1_X x ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
linked t1 ->
sconst t2 ->
- cinits t ->
- valid_rd t1 a 3 -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rw t1 a 3
+ cinits t -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rd t1 a 3
end
[wp:print-generated]
@@ -279,25 +279,25 @@ end
(* use frama_c_wp.memaddr.MemAddr *)
- (* use S1_X *)
-
(* use Chunk *)
(* use frama_c_wp.memory.Memory *)
+ (* use S1_X *)
+
(* use Compound *)
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
- addr -> int, a:addr, x:S1_X.
+ addr -> int, a:addr.
region (a.base) <= 0 ->
- IsS1_X x ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
linked t1 ->
sconst t2 ->
- cinits t -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rd t1 a 3
+ cinits t ->
+ valid_rd t1 a 3 -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rw t1 a 3
end
[wp] 2 goals generated
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
index 9d8062124cf..da51a2ee8e0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
@@ -36,6 +36,28 @@ theory A_A
predicate P_P A_InAxiomatic
end
+[wp:print-generated]
+ theory WP
+
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use A_A *)
+
+ goal wp_goal : forall i:A_InAxiomatic. is_InAxiomatic i -> P_P i
+
+ end
---------------------------------------------
--- Context 'typed' Cluster 'Axiomatic1'
---------------------------------------------
@@ -96,6 +118,30 @@ theory A_X
predicate P_Q A_AtTopLevel
end
+[wp:print-generated]
+ theory WP1
+
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use Axiomatic1 *)
+
+ (* use A_X *)
+
+ goal wp_goal : forall a:A_AtTopLevel. is_AtTopLevel a -> P_Q a
+
+ end
---------------------------------------------
--- Context 'typed' Cluster 'Axiomatic2'
---------------------------------------------
@@ -158,7 +204,7 @@ theory A_Y
end
[wp:print-generated]
- theory WP
+ theory WP2
(* use why3.BuiltIn.BuiltIn *)
@@ -180,52 +226,6 @@ end
goal wp_goal : forall r:A_Rec. is_Rec r -> P_R r
- end
-[wp:print-generated]
- theory WP1
-
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use Axiomatic1 *)
-
- (* use A_X *)
-
- goal wp_goal : forall a:A_AtTopLevel. is_AtTopLevel a -> P_Q a
-
- end
-[wp:print-generated]
- theory WP2
-
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use A_A *)
-
- goal wp_goal : forall i:A_InAxiomatic. is_InAxiomatic i -> P_P i
-
end
[wp] 3 goals generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
index 1e18cbcb41b..da0b8cd094c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
@@ -35,7 +35,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTP (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNE (of_f64 f))
end
[wp:print-generated]
@@ -66,7 +66,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTZ (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNA (of_f64 f))
end
[wp:print-generated]
@@ -97,7 +97,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNA (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTZ (of_f64 f))
end
[wp:print-generated]
@@ -128,7 +128,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
- forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RNE (of_f64 f))
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTP (of_f64 f))
end
[wp:print-generated]
@@ -158,7 +158,8 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal : forall f:t. is_NaN_f64 (add_f64 f (0x1.0p0:t))
+ goal wp_goal :
+ forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTN (of_f64 f))
end
[wp:print-generated]
@@ -188,7 +189,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal : forall f:t. is_infinite_f64 (add_f64 f (0x1.0p0:t))
+ goal wp_goal : forall f:t. is_finite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
@@ -218,7 +219,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal : forall f:t. is_finite_f64 (add_f64 f (0x1.0p0:t))
+ goal wp_goal : forall f:t. is_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
@@ -248,8 +249,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t. eq_f64 (add_f64 f (0x1.0p0:t)) (round_double RTN (of_f64 f))
+ goal wp_goal : forall f:t. is_NaN_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
@@ -257,31 +257,29 @@
(* use why3.BuiltIn.BuiltIn *)
- (* use bool.Bool1 *)
+ (* use bool.Bool *)
- (* use int.Int1 *)
+ (* use int.Int *)
- (* use int.ComputerDivision1 *)
+ (* use int.ComputerDivision *)
- (* use real.RealInfix1 *)
+ (* use real.RealInfix *)
- (* use frama_c_wp.qed.Qed1 *)
+ (* use frama_c_wp.qed.Qed *)
- (* use map.Map1 *)
+ (* use map.Map *)
- (* use real.Abs1 *)
+ (* use real.Abs *)
- (* use frama_c_wp.cmath.Cmath1 *)
+ (* use frama_c_wp.cmath.Cmath *)
- (* use real.Square2 *)
+ (* use real.Square *)
- (* use frama_c_wp.cmath.Square3 *)
+ (* use frama_c_wp.cmath.Square1 *)
- (* use frama_c_wp.cfloat.Cfloat1 *)
+ (* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t1.
- eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNA1 (of_f32 f))
+ goal wp_goal : forall f:t. is_positive_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
@@ -289,31 +287,29 @@
(* use why3.BuiltIn.BuiltIn *)
- (* use bool.Bool1 *)
+ (* use bool.Bool *)
- (* use int.Int1 *)
+ (* use int.Int *)
- (* use int.ComputerDivision1 *)
+ (* use int.ComputerDivision *)
- (* use real.RealInfix1 *)
+ (* use real.RealInfix *)
- (* use frama_c_wp.qed.Qed1 *)
+ (* use frama_c_wp.qed.Qed *)
- (* use map.Map1 *)
+ (* use map.Map *)
- (* use real.Abs1 *)
+ (* use real.Abs *)
- (* use frama_c_wp.cmath.Cmath1 *)
+ (* use frama_c_wp.cmath.Cmath *)
- (* use real.Square2 *)
+ (* use real.Square *)
- (* use frama_c_wp.cmath.Square3 *)
+ (* use frama_c_wp.cmath.Square1 *)
- (* use frama_c_wp.cfloat.Cfloat1 *)
+ (* use frama_c_wp.cfloat.Cfloat *)
- goal wp_goal :
- forall f:t1.
- eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNE1 (of_f32 f))
+ goal wp_goal : forall f:t. is_negative_infinite_f64 (add_f64 f (0x1.0p0:t))
end
[wp:print-generated]
@@ -321,29 +317,31 @@
(* use why3.BuiltIn.BuiltIn *)
- (* use bool.Bool *)
+ (* use bool.Bool1 *)
- (* use int.Int *)
+ (* use int.Int1 *)
- (* use int.ComputerDivision *)
+ (* use int.ComputerDivision1 *)
- (* use real.RealInfix *)
+ (* use real.RealInfix1 *)
- (* use frama_c_wp.qed.Qed *)
+ (* use frama_c_wp.qed.Qed1 *)
- (* use map.Map *)
+ (* use map.Map1 *)
- (* use real.Abs *)
+ (* use real.Abs1 *)
- (* use frama_c_wp.cmath.Cmath *)
+ (* use frama_c_wp.cmath.Cmath1 *)
- (* use real.Square *)
+ (* use real.Square2 *)
- (* use frama_c_wp.cmath.Square1 *)
+ (* use frama_c_wp.cmath.Square3 *)
- (* use frama_c_wp.cfloat.Cfloat *)
+ (* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t. is_negative_infinite_f64 (add_f64 f (0x1.0p0:t))
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNE1 (of_f32 f))
end
[wp:print-generated]
@@ -351,29 +349,31 @@
(* use why3.BuiltIn.BuiltIn *)
- (* use bool.Bool *)
+ (* use bool.Bool1 *)
- (* use int.Int *)
+ (* use int.Int1 *)
- (* use int.ComputerDivision *)
+ (* use int.ComputerDivision1 *)
- (* use real.RealInfix *)
+ (* use real.RealInfix1 *)
- (* use frama_c_wp.qed.Qed *)
+ (* use frama_c_wp.qed.Qed1 *)
- (* use map.Map *)
+ (* use map.Map1 *)
- (* use real.Abs *)
+ (* use real.Abs1 *)
- (* use frama_c_wp.cmath.Cmath *)
+ (* use frama_c_wp.cmath.Cmath1 *)
- (* use real.Square *)
+ (* use real.Square2 *)
- (* use frama_c_wp.cmath.Square1 *)
+ (* use frama_c_wp.cmath.Square3 *)
- (* use frama_c_wp.cfloat.Cfloat *)
+ (* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t. is_positive_infinite_f64 (add_f64 f (0x1.0p0:t))
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RNA1 (of_f32 f))
end
[wp:print-generated]
@@ -403,7 +403,9 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t1. is_finite_f32 (add_f32 f (0x1.0p0:t1))
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTZ1 (of_f32 f))
end
[wp:print-generated]
@@ -435,7 +437,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTN1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTP1 (of_f32 f))
end
[wp:print-generated]
@@ -467,7 +469,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTP1 (of_f32 f))
+ eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTN1 (of_f32 f))
end
[wp:print-generated]
@@ -497,9 +499,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal :
- forall f:t1.
- eq_f32 (add_f32 f (0x1.0p0:t1)) (round_float RTZ1 (of_f32 f))
+ goal wp_goal : forall f:t1. is_finite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
@@ -529,8 +529,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal :
- forall f:t1. is_negative_infinite_f32 (add_f32 f (0x1.0p0:t1))
+ goal wp_goal : forall f:t1. is_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
@@ -560,8 +559,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal :
- forall f:t1. is_positive_infinite_f32 (add_f32 f (0x1.0p0:t1))
+ goal wp_goal : forall f:t1. is_NaN_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
@@ -591,7 +589,8 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t1. is_NaN_f32 (add_f32 f (0x1.0p0:t1))
+ goal wp_goal :
+ forall f:t1. is_positive_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp:print-generated]
@@ -621,7 +620,8 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
- goal wp_goal : forall f:t1. is_infinite_f32 (add_f32 f (0x1.0p0:t1))
+ goal wp_goal :
+ forall f:t1. is_negative_infinite_f32 (add_f32 f (0x1.0p0:t1))
end
[wp] 20 goals generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index c5b596fd478..3d7336db000 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -59,51 +59,12 @@ end
P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root))
node -> P_reachable malloc mptr root node
- goal wp_goal :
- forall t:int -> int, t1:addr -> addr, a:addr, a1:addr.
- P_reachable t t1 a1 a ->
- a1 = a \/
- valid_rw t a1 2 /\
- P_reachable t t1 (get t1 (shiftfield_F1__list_next a1)) a
-
- end
-[wp:print-generated]
- theory WP1
-
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use frama_c_wp.memaddr.MemAddr *)
-
- (* use Compound *)
-
- inductive P_reachable1 (int -> int) (addr -> addr) addr addr =
- | Q_root_reachable1 :
- forall malloc:int -> int, mptr:addr -> addr, root:addr.
- P_reachable1 malloc mptr root root
- | Q_next_reachable1 :
- forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
- valid_rw malloc root 2 ->
- P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root))
- node -> P_reachable1 malloc mptr root node
-
lemma Q_test :
forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
- P_reachable1 malloc mptr root node ->
+ P_reachable malloc mptr root node ->
root = node \/
valid_rw malloc root 2 /\
- P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node
+ P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node
predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
addr) (begin1:int) (end1:int) =
@@ -149,6 +110,45 @@ end
P_same_elements t t1 (shift_sint32 a i2) (shift_sint32 a1 i2) i i1 ->
P_same_elements t t1 a a1 (i + i2) (i1 + i2)
+ end
+[wp:print-generated]
+ theory WP1
+
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memaddr.MemAddr *)
+
+ (* use Compound *)
+
+ inductive P_reachable1 (int -> int) (addr -> addr) addr addr =
+ | Q_root_reachable1 :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr.
+ P_reachable1 malloc mptr root root
+ | Q_next_reachable1 :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+ valid_rw malloc root 2 ->
+ P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root))
+ node -> P_reachable1 malloc mptr root node
+
+ goal wp_goal :
+ forall t:int -> int, t1:addr -> addr, a:addr, a1:addr.
+ P_reachable1 t t1 a1 a ->
+ a1 = a \/
+ valid_rw t a1 2 /\
+ P_reachable1 t t1 (get t1 (shiftfield_F1__list_next a1)) a
+
end
[wp] 2 goals generated
------------------------------------------------------------
--
GitLab