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

Merge branch 'feature/patrick/wp-multidimentional-arrays' into 'master' 

[WP/test] adding a test initializing multidimentianal arrays

See merge request frama-c/frama-c!2167
parents 2e263cb2 509f2b79
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 4681 additions and 54 deletions
src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+ 1950
− 10
View file @ 09dad77a
This diff is collapsed.
src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+ 1950
− 10
View file @ 09dad77a
This diff is collapsed.
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
+ 213
− 4
View file @ 09dad77a
{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 19 }, { "wp:global": { "alt-ergo": { "total": 27, "valid": 16, "unknown": 11,
"qed": { "total": 4, "valid": 4 }, "rank": 19 },
"wp:main": { "total": 8, "valid": 8, "rank": 19 } }, "qed": { "total": 27, "valid": 27 },
"wp:main": { "total": 54, "valid": 43, "unknown": 11,
"rank": 19 } },
"wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo": "wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo":
{ "total": 1, { "total": 1,
"valid": 1, "valid": 1,
...@@ -47,4 +49,211 @@ ...@@ -47,4 +49,211 @@
"valid": 4 }, "valid": 4 },
"wp:main": { "total": 8, "wp:main": { "total": 8,
"valid": 8, "valid": 8,
"rank": 19 } } } } } "rank": 19 } } },
"init_t1": { "init_t1_loop_invariant_Partial": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 4 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 4 } },
"init_t1_loop_invariant_Range": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 2 } },
"init_t1_assigns": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
"init_t1_loop_assigns": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_t1_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 3 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 3 } },
"wp:section": { "alt-ergo": { "total": 3,
"valid": 3,
"rank": 4 },
"qed": { "total": 5,
"valid": 5 },
"wp:main": { "total": 8,
"valid": 8,
"rank": 4 } } },
"init_t2": { "init_t2_assert_i": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_assert_j": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_loop_invariant_Previous_i":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 5 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 5 } },
"init_t2_loop_invariant_Partial_j":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 8 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 8 } },
"init_t2_loop_invariant_Range_j": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 3 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 3 } },
"init_t2_loop_invariant_Partial_i":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 11 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 11 } },
"init_t2_loop_invariant_Range_i": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 2 } },
"init_t2_assigns": { "alt-ergo": { "total": 1,
"unknown": 1 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
"valid": 1,
"unknown": 1 } },
"init_t2_loop_assigns_2": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_loop_assigns": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 2 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 2 } },
"wp:section": { "alt-ergo": { "total": 11,
"valid": 6,
"unknown": 5,
"rank": 11 },
"qed": { "total": 10,
"valid": 10 },
"wp:main": { "total": 21,
"valid": 16,
"unknown": 5,
"rank": 11 } } },
"init_t2_bis": { "init_requires_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_requires": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_bis_assert_i": { "qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_t2_bis_loop_invariant_Partial_i":
{ "alt-ergo": { "total": 1,
"valid": 1,
"rank": 10 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 10 } },
"init_t2_bis_loop_invariant_Range_i":
{ "alt-ergo": { "total": 1,
"valid": 1,
"rank": 3 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 3 } },
"init_t2_bis_assigns": { "alt-ergo":
{ "total": 3,
"unknown": 3 },
"qed":
{ "total": 2,
"valid": 2 },
"wp:main":
{ "total": 5,
"valid": 2,
"unknown": 3 } },
"init_t2_bis_loop_assigns": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_bis_exits": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"init_t2_bis_ensures": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 3 },
"wp:main":
{ "total": 1,
"valid": 1,
"rank": 3 } },
"wp:section": { "alt-ergo": { "total": 9,
"valid": 3,
"unknown": 6,
"rank": 10 },
"qed": { "total": 8,
"valid": 8 },
"wp:main": { "total": 17,
"valid": 11,
"unknown": 6,
"rank": 10 } } } } }
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle 0 → 100644
+ 117
− 0
View file @ 09dad77a
# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 91 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns : Valid
[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t1_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_t1_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_t1_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_t1_loop_assigns : Valid
[wp] [Qed] Goal typed_init_t1_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_t1_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_init_t1_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t1_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_ensures : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_exits : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_assert_Offset : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_loop_variant_positive : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_call_init_requires : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_call_init_requires_2 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_ensures : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_exits : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_assert_Offset_i : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_variant_positive : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires_2 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Partial_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Partial_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Range_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Range_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Partial_j_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Partial_j_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Previous_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Previous_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Range_j_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Range_j_established : Valid
[wp] [Qed] Goal typed_init_t2_v1_assert_Last_j : Valid
[wp] [Qed] Goal typed_init_t2_v1_assert_Last_i : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v1_loop_variant_2_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Partial_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Partial_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Range_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Range_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Partial_j_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Partial_j_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Previous_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Previous_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Range_j_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Range_j_established : Valid
[wp] [Qed] Goal typed_init_t2_v2_assert_Last_j : Valid
[wp] [Qed] Goal typed_init_t2_v2_assert_Last_i : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_variant_2_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Partial_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Partial_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Range_i_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Range_i_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Partial_j_preserved : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Partial_j_established : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Range_j_preserved : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Range_j_established : Valid
[wp] [Qed] Goal typed_init_t2_v3_assert_Last_j : Valid
[wp] [Qed] Goal typed_init_t2_v3_assert_Last_i : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_variant_2_positive : Valid
[wp] Proved goals: 91 / 91
Qed: 51
Alt-Ergo: 40
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 6 4 (80..104) 10 100%
init_t1 6 4 (12..24) 10 100%
init_t2_v1 9 8 (40..52) 17 100%
init_t2_v2 9 8 (32..44) 17 100%
init_t2_v3 7 8 (28..40) 15 100%
init_t2_bis_v1 7 4 (208..256) 11 100%
init_t2_bis_v2 7 4 (192..240) 11 100%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle 0 → 100644
+ 49
− 0
View file @ 09dad77a
# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1'
[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1/wp'
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_normal_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_assigns_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_t2_v2_loop_assigns_2_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_2_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_2_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_assigns_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v2_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_2_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_2_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_v3_assigns_part1 : Valid
[wp] [Tactical] Goal typed_init_t2_v3_assigns_part2 : Valid
[wp] Proved goals: 23 / 23
Qed: 11
Alt-Ergo: 0 (unsuccess: 12)
Script: 12
[wp] Updated session with 12 new valid scripts.
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.1.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v2 3 - (16..28) 8 100%
init_t2_v3 4 - (20..32) 7 100%
init_t2_bis_v2 4 - (28..40) 8 100%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle 0 → 100644
+ 37
− 0
View file @ 09dad77a
# frama-c -wp -wp-timeout 90 -wp-steps 300 [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_init_t2_bis_v1_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_assigns_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_assigns_part3 : Unsuccess
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_exit_part2 : Unsuccess
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_normal_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_normal_part2 : Unsuccess
[wp] [Qed] Goal typed_init_t2_v1_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_part3 : Unsuccess
[wp] [Qed] Goal typed_init_t2_v1_loop_assigns_2_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_2_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_2_part3 : Unsuccess
[wp] [Qed] Goal typed_init_t2_v1_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v1_assigns_part2 : Unsuccess
[wp] Proved goals: 7 / 16
Qed: 7
Alt-Ergo: 0 (unsuccess: 9)
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.2.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.2.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v1 3 - 8 37.5%
init_t2_bis_v1 4 - 8 50.0%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.i.0.report.json
+ 213
− 4
View file @ 09dad77a
{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 19 }, { "wp:global": { "alt-ergo": { "total": 27, "valid": 16, "unknown": 11,
"qed": { "total": 4, "valid": 4 }, "rank": 19 },
"wp:main": { "total": 8, "valid": 8, "rank": 19 } }, "qed": { "total": 27, "valid": 27 },
"wp:main": { "total": 54, "valid": 43, "unknown": 11,
"rank": 19 } },
"wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo": "wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo":
{ "total": 1, { "total": 1,
"valid": 1, "valid": 1,
...@@ -47,4 +49,211 @@ ...@@ -47,4 +49,211 @@
"valid": 4 }, "valid": 4 },
"wp:main": { "total": 8, "wp:main": { "total": 8,
"valid": 8, "valid": 8,
"rank": 19 } } } } } "rank": 19 } } },
"init_t1": { "init_t1_loop_invariant_Partial": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 4 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 4 } },
"init_t1_loop_invariant_Range": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 2 } },
"init_t1_assigns": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
"init_t1_loop_assigns": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_t1_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 3 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 3 } },
"wp:section": { "alt-ergo": { "total": 3,
"valid": 3,
"rank": 4 },
"qed": { "total": 5,
"valid": 5 },
"wp:main": { "total": 8,
"valid": 8,
"rank": 4 } } },
"init_t2": { "init_t2_assert_i": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_assert_j": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_loop_invariant_Previous_i":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 5 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 5 } },
"init_t2_loop_invariant_Partial_j":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 8 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 8 } },
"init_t2_loop_invariant_Range_j": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 3 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 3 } },
"init_t2_loop_invariant_Partial_i":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 11 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 11 } },
"init_t2_loop_invariant_Range_i": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
"rank": 2 } },
"init_t2_assigns": { "alt-ergo": { "total": 1,
"unknown": 1 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
"valid": 1,
"unknown": 1 } },
"init_t2_loop_assigns_2": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_loop_assigns": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 2 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 2 } },
"wp:section": { "alt-ergo": { "total": 11,
"valid": 6,
"unknown": 5,
"rank": 11 },
"qed": { "total": 10,
"valid": 10 },
"wp:main": { "total": 21,
"valid": 16,
"unknown": 5,
"rank": 11 } } },
"init_t2_bis": { "init_requires_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_requires": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"init_t2_bis_assert_i": { "qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"init_t2_bis_loop_invariant_Partial_i":
{ "alt-ergo": { "total": 1,
"valid": 1,
"rank": 10 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 10 } },
"init_t2_bis_loop_invariant_Range_i":
{ "alt-ergo": { "total": 1,
"valid": 1,
"rank": 3 },
"qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 2, "valid": 2,
"rank": 3 } },
"init_t2_bis_assigns": { "alt-ergo":
{ "total": 3,
"unknown": 3 },
"qed":
{ "total": 2,
"valid": 2 },
"wp:main":
{ "total": 5,
"valid": 2,
"unknown": 3 } },
"init_t2_bis_loop_assigns": { "alt-ergo":
{ "total": 2,
"unknown": 2 },
"qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 3,
"valid": 1,
"unknown": 2 } },
"init_t2_bis_exits": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"init_t2_bis_ensures": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 3 },
"wp:main":
{ "total": 1,
"valid": 1,
"rank": 3 } },
"wp:section": { "alt-ergo": { "total": 9,
"valid": 3,
"unknown": 6,
"rank": 10 },
"qed": { "total": 8,
"valid": 8 },
"wp:main": { "total": 17,
"valid": 11,
"unknown": 6,
"rank": 10 } } } } }
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle deleted 100644 → 0
+ 0
− 23
View file @ 2e263cb2
# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns : Valid
[wp] Proved goals: 8 / 8
Qed: 4
Alt-Ergo: 4
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 4 4 (80..104) 8 100%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/user_init.i
+ 152
− 3
View file @ 09dad77a
/* run.config_qualif
EXECNOW: rm -rf @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-1/
OPT: -wp-prop=-lack,-tactic
OPT: -wp-prop=tactic -wp-auto=wp:split -session @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-@PTEST_NUMBER@
OPT: -wp-prop=lack -wp-steps 300
*/
/*@ requires \valid(a+(0..n-1)) ; /*@ requires \valid(a+(0..n-1)) ;
@ requires n >= 0 ; @ requires n >= 0 ;
@ ensures \forall int k ; 0 <= k < n ==> a[k] == v ;
@ assigns a[0..n-1] ; @ assigns a[0..n-1] ;
@ ensures \forall int k ; 0 <= k < n ==> a[k] == v ;
@ exits \false;
*/ */
void init( int * a , int n , int v ) void init( int * a , int n , int v )
{ {
/*@ loop invariant Range: 0 <= i <= n ; /*@ loop assigns Zone: i,a[0..n-1] ;
@ loop invariant Range: 0 <= i <= n ;
@ loop invariant Partial: \forall int k ; 0 <= k < i ==> a[k] == v ; @ loop invariant Partial: \forall int k ; 0 <= k < i ==> a[k] == v ;
@ loop assigns i,a[0..n-1] ; @ loop variant Decr_i: n - i ;
*/ */
for (int i = 0 ; i < n ; i++) a[i] = v ; for (int i = 0 ; i < n ; i++) a[i] = v ;
} }
//-------------------------
int t1[10];
/*@ ensures \forall integer k; 0 <= k < 10 ==> t1[k] == v ;
@ exits \false;
@ assigns t1[0..9] ;
*/
void init_t1(int v) {
unsigned i;
/*@ loop assigns Zone: i,t1[0..9] ;
@ loop invariant Range: 0 <= i <= 10 ;
@ loop invariant Partial: \forall integer k ; 0 <= k < i ==> t1[k] ≡ v ;
@ loop variant Decr: 10 - i ;
*/
for (i = 0 ; i < 10 ; i++) t1[i] = v ;
}
//-------------------------
int t2[10][20];
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
@ exits \false;
@ assigns lack: t2[0..9][0..19];
*/
void init_t2_v1(int v) {
unsigned i,j;
/*@ loop assigns lack: Zone_i: i, j, t2[0..9][0..19];
@ loop invariant Range_i: 0 <= i <= 10 ;
@ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
@ loop variant Decr_i: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
/*@ loop assigns lack: Zone_j: j, t2[0..9][0..19];
@ loop invariant Range_j: 0 <= j <= 20 ;
@ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
@ loop invariant Previous_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == \at(t2[k][l], LoopEntry);
@ loop variant Decr_j: 20 - j ;
*/
for(j = 0; j <= 19; j++) {
t2[i][j] = v;
}
//@ assert Last_j: j==20;
;
}
//@ assert Last_i: i==10;
;
}
//-------------------------
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
@ exits \false;
@ assigns tactic: t2[..][..];
*/
void init_t2_v2(int v) {
unsigned i,j;
/*@ loop assigns tactic: Zone_i: i, j, t2[..][..];
@ loop invariant Range_i: 0 <= i <= 10 ;
@ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
@ loop variant Decr_i: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
/*@ loop assigns tactic: Zone_j: j, t2[..][..];
@ loop invariant Range_j: 0 <= j <= 20 ;
@ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
@ loop invariant Previous_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == \at(t2[k][l], LoopEntry);
@ loop variant Decr_j: 20 - j ;
*/
for(j = 0; j <= 19; j++) {
t2[i][j] = v;
}
//@ assert Last_j: j==20;
;
}
//@ assert Last_i: i==10;
;
}
//-------------------------
//@ predicate MemSet20(int t2[20], integer n, integer v) = n <= 20 && \forall integer k ; 0 <= k < n ==> t2[k] == v;
/*@ ensures \forall integer k; 0 <= k < 10 ==> MemSet20(t2[k], 20, v);
@ exits \false;
@ assigns tactic: t2[..][..];
*/
void init_t2_v3(int v) {
unsigned i,j;
/*@ loop assigns tactic: Zone_i: i, j, t2[..][..];
@ loop invariant Range_i: 0 <= i <= 10 ;
@ loop invariant Partial_i: \forall integer k; 0 <= k < i ==> MemSet20(t2[k], 20, v);
@ loop variant V_i: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
/*@ loop assigns tactic: Zone_j: j, t2[i][..];
@ loop invariant Range_j: 0 <= j <= 20 ;
@ loop invariant Partial_j: MemSet20(t2[i], j, v);
@ loop variant Decr_j: 20 - j ;
*/
for(j = 0; j <= 19; j++) {
t2[i][j] = v;
}
//@ assert Last_j: j==20;
;
}
//@ assert Last_i: i==10;
;
}
//-------------------------
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
@ assigns lack: t2[0..9][0..19];
@ exits \false;
*/
void init_t2_bis_v1(int v) {
unsigned i;
/*@ loop assigns lack: Zone: i, t2[0..9][0..19];
@ loop invariant Range: 0 <= i <= 10 ;
@ loop invariant Partial: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
@ loop variant Decr: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
init(&t2[i][0], 20, v);
//@ assert Offset: &t2[i][0] == &t2[0][0] + 20*i;
}
}
//-------------------------
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
@ assigns tactic: t2[..][..];
@ exits \false;
*/
void init_t2_bis_v2(int v) {
unsigned i;
/*@ loop assigns tactic: Zone: i, t2[..][..];
@ loop invariant Range: 0 <= i <= 10 ;
@ loop invariant Partial: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
@ loop variant Decr: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
init(&t2[i][0], 20, v);
//@ assert Offset_i: &t2[i][0] == &t2[0][0] + 20*i;
;
}
}
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