Skip to content
Snippets Groups Projects
Commit a3b60b27 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp/tests] no more need of +cast for a test

parent 3c0bc02a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_acsl/logic.i
+ 2
− 2
View file @ a3b60b27
/* run.config /* run.config
OPT: -wp-model Typed+cast OPT: -wp-model Typed
*/ */
/* run.config_qualif /* run.config_qualif
OPT: -wp -wp-model Typed+cast -wp-steps 50 OPT: -wp -wp-model Typed -wp-steps 50
*/ */
// Test logic types defined from C types // Test logic types defined from C types
//-------------------------------------- //--------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+ 20
− 23
View file @ a3b60b27
# frama-c -wp -wp-model 'Typed (Cast)' [...] # frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing) [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
...@@ -66,19 +66,18 @@ Let a = global(G_tr_31). ...@@ -66,19 +66,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift___anonstruct_Point_1(a, 0).
Let a_4 = global(G_buint_37). Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let a_5 = shiftfield_F4_bytes(a_4).
Let m = Array1_S1(a_3, 3, Mint_0). Let m = Array1_S1(a_3, 3, Mint_0).
Assume { Assume {
Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m). Type: IsArray1S1(m).
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1. Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 1)] = 2. Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 2)] = 4. Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 3)] = 8. Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *) (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10. Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *) (* Initializer *)
...@@ -103,19 +102,18 @@ Let a = global(G_tr_31). ...@@ -103,19 +102,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift___anonstruct_Point_1(a, 0).
Let a_4 = global(G_buint_37). Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let a_5 = shiftfield_F4_bytes(a_4).
Let m = Array1_S1(a_3, 3, Mint_0). Let m = Array1_S1(a_3, 3, Mint_0).
Assume { Assume {
Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m). Type: IsArray1S1(m).
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1. Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 1)] = 2. Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 2)] = 4. Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 3)] = 8. Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *) (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10. Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *) (* Initializer *)
...@@ -140,19 +138,18 @@ Let a = global(G_tr_31). ...@@ -140,19 +138,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2). Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1). Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0). Let a_3 = shift___anonstruct_Point_1(a, 0).
Let a_4 = global(G_buint_37). Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let a_5 = shiftfield_F4_bytes(a_4).
Let m = Array1_S1(a_3, 3, Mint_0). Let m = Array1_S1(a_3, 3, Mint_0).
Assume { Assume {
Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m). Type: IsArray1S1(m).
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1. Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 1)] = 2. Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 2)] = 4. Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 3)] = 8. Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *) (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10. Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *) (* Initializer *)
...@@ -238,7 +235,7 @@ Let a_4 = global(G_buint_37). ...@@ -238,7 +235,7 @@ Let a_4 = global(G_buint_37).
Let a_5 = shiftfield_F4_bytes(a_4). Let a_5 = shiftfield_F4_bytes(a_4).
Let a_6 = Load_S4(a_4, Mint_0). Let a_6 = Load_S4(a_4, Mint_0).
Assume { Assume {
Type: is_uint32(Mint_0[a_4]) /\ IsS4(a_6). Type: IsS4(a_6).
(* Initializer *) (* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1. Init: Mint_0[shift_uint8(a_5, 0)] = 1.
(* Initializer *) (* Initializer *)
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+ 22
− 22
View file @ a3b60b27
# frama-c -wp -wp-model 'Typed (Cast)' -wp-timeout 90 -wp-steps 50 [...] # frama-c -wp -wp-timeout 90 -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing) [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver' [wp] Loading driver 'share/wp.driver'
...@@ -35,27 +35,27 @@ ...@@ -35,27 +35,27 @@
[wp] tests/wp_acsl/logic.i:62: Warning: [wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled [wp] 21 goals scheduled
[wp] [Qed] Goal typed_cast_h_ensures : Valid [wp] [Qed] Goal typed_h_ensures : Valid
[wp] [Qed] Goal typed_cast_h_assigns_exit : Valid [wp] [Qed] Goal typed_h_assigns_exit : Valid
[wp] [Qed] Goal typed_cast_h_assigns_normal : Valid [wp] [Qed] Goal typed_h_assigns_normal : Valid
[wp] [Qed] Goal typed_cast_main_requires_qed_ok : Valid [wp] [Qed] Goal typed_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_2 : Unsuccess [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_3 : Unsuccess [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_4 : Unsuccess [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_5 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_6 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_7 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_8 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_8 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_9 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_9 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_10 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_10 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_11 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_11 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_12 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_12 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_13 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_13 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_14 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_14 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_15 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_15 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_16 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_17 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_18 : Unsuccess (Stronger) [wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
[wp] Proved goals: 4 / 21 [wp] Proved goals: 4 / 21
Qed: 4 Qed: 4
Alt-Ergo: 0 (unsuccess: 17) Alt-Ergo: 0 (unsuccess: 17)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment