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

Merge branch 'feature/wp/dune-tests' into 'feature/bobot/jbuilder' 

[wp] Enable WP tests in Dune

See merge request frama-c/frama-c!3633
parents 82bea003 53967ef5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 16 additions and 772 deletions
src/plugins/wp/tests/ptests_config
+ 4
− 7
View file @ 834c4a23
# todo: to fixe # todo: to fixe
IGNORE= DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
IGNORE= DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
IGNORE= DEFAULT_SUITES= wp_region qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip why3
IGNORE= qualif_SUITES= wp wp_plugin wp_acsl wp_bts wp_store wp_hoare
IGNORE= qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip wp_region
IGNORE= qualif_SUITES= why3
src/plugins/wp/tests/test_config
+ 2
− 1
View file @ 834c4a23
PLUGIN: wp PLUGIN: wp
MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
MACRO: USING_WP_SESSION -wp-session @WP_SESSION@ MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive" 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"
OPT: OPT:
src/plugins/wp/tests/test_config_qualif
+ 2
− 1
View file @ 834c4a23
PLUGIN: wp PLUGIN: wp
MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
MACRO: USING_WP_SESSION -wp-session @WP_SESSION@ MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@ COMMENT: no need of "-wp-share" in Dune -> Dune finds it automatically
CMD: @frama-c@ -wp -wp-par 1 -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@
OPT: OPT:
src/plugins/wp/tests/wp_bts/issue_143.i deleted 100644 → 0
+ 0
− 22
View file @ 82bea003
/* run.config
DONTRUN:
*/
/* run.config_qualif
CMD: chmod a-x %{dep:../../inexistant-prover} && @frama-c@ @WP_OPTIONS@ @PTEST_OPTIONS@
OPT: -wp
OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo %{dep:../../inexistant-prover} -wp-coqc %{dep:../../inexistant-prover}
OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo %{dep:../../inexistant-prover}
OPT: -wp -wp-prover "native:coq" -wp-coqc %{dep:../../inexistant-prover}
*/
/*@
axiomatic A {
lemma ok_because_inconsistent: \forall integer x; x > 0 ==> x < 0 ==> x == 0 ;
}
*/
/*@
axiomatic B {
lemma ok_because_consistent: \forall integer x; x > 0 ==> x*x > 0 ;
}
*/
src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle deleted 100644 → 0
+ 0
− 10
View file @ 82bea003
# frama-c -wp -wp-rte -wp-steps 50 [...]
[kernel] Parsing issue_141.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function f
[rte] annotating function main
[wp] issue_141.i:18: Warning:
calculus failed on strategy
for 'main', behavior 'default!', all properties, both assigns or not because
unsupported strange loop(s). (abort)
[wp] No proof obligations
src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle deleted 100644 → 0
+ 0
− 14
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing bts_2471.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
[wp] [Coq (native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
Coq (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 1 0.0%
------------------------------------------------------------
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle deleted 100644 → 0
+ 0
− 14
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic A - 1 1 100%
Axiomatic B - 1 1 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle deleted 100644 → 0
+ 0
− 15
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic A - 1 1 100%
Axiomatic B - 1 1 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle deleted 100644 → 0
+ 0
− 14
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic A - 1 1 100%
Axiomatic B - 1 1 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle deleted 100644 → 0
+ 0
− 17
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Coq (native)] Goal typed_lemma_ok_because_consistent : Failed
Command '../../inexistant-prover' not found
[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
[wp] [Coq (native)] Goal typed_lemma_ok_because_inconsistent : Failed
Command '../../inexistant-prover' not found
[wp] Proved goals: 0 / 2
Coq (native): 0 (failed: 2)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic A - - 1 0.0%
Axiomatic B - - 1 0.0%
------------------------------------------------------------
src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle deleted 100644 → 0
+ 0
− 18
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing issue_453.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_f1_loop_assigns : Valid
[wp] [Qed] Goal typed_f1_ensures_Sincr : Valid
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Qed] Goal typed_f2_loop_assigns : Valid
[wp] [Qed] Goal typed_f2_ensures_Sincr : Valid
[wp] [Qed] Goal typed_f2_assigns : Valid
[wp] Proved goals: 6 / 6
Qed: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f1 3 - 3 100%
f2 3 - 3 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+ 1
− 1
View file @ 834c4a23
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
*/ */
/* run.config_qualif /* run.config_qualif
DEPS: @WP_SESSION@/script/*
OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@ OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@
*/ */
......
src/plugins/wp/tests/wp_gallery/dune 0 → 100644
+ 3
− 0
View file @ 834c4a23
(subdir
result_qualif/binary-multiplication.0.session_qualif/script
(copy_files ../../../binary-multiplication.0.session_qualif/script/*))
src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle deleted 100644 → 0
+ 0
− 153
View file @ 82bea003
# frama-c -wp -wp-rte [...]
[kernel] Parsing frama_c_hashtbl_solved.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function add
[rte] annotating function eq_string
[rte] annotating function hash
[rte] annotating function init
[rte] annotating function mem_binding
[rte] annotating function size
[wp] Goal typed_eq_string_complete_eq_not_eq : trivial
[wp] Goal typed_eq_string_disjoint_eq_not_eq : trivial
[wp] Goal typed_eq_string_loop_invariant_preserved : not tried
[wp] Goal typed_eq_string_loop_invariant_established : not tried
[wp] Goal typed_eq_string_loop_invariant_2_preserved : not tried
[wp] Goal typed_eq_string_loop_invariant_2_established : not tried
[wp] Goal typed_eq_string_assert_rte_mem_access : not tried
[wp] Goal typed_eq_string_assert_rte_mem_access_2 : not tried
[wp] Goal typed_eq_string_assert_rte_signed_overflow : not tried
[wp] Goal typed_eq_string_loop_assigns : trivial
[wp] Goal typed_eq_string_assigns_part1 : not tried
[wp] Goal typed_eq_string_assigns_part2 : not tried
[wp] Goal typed_eq_string_assigns_part3 : not tried
[wp] Goal typed_eq_string_assigns_part4 : not tried
[wp] Goal typed_eq_string_loop_variant_decrease : not tried
[wp] Goal typed_eq_string_loop_variant_positive : not tried
[wp] Goal typed_eq_string_eq_ensures : not tried
[wp] Goal typed_eq_string_not_eq_ensures : not tried
[wp] Goal typed_hash_ensures_left_unproved : not tried
[wp] Goal typed_hash_loop_invariant_preserved : not tried
[wp] Goal typed_hash_loop_invariant_established : not tried
[wp] Goal typed_hash_assert_rte_mem_access : not tried
[wp] Goal typed_hash_assert_rte_mem_access_2 : not tried
[wp] Goal typed_hash_assert_rte_signed_overflow : not tried
[wp] Goal typed_hash_loop_assigns : trivial
[wp] Goal typed_hash_assigns_part1 : not tried
[wp] Goal typed_hash_assigns_part2 : not tried
[wp] Goal typed_hash_loop_variant_decrease : not tried
[wp] Goal typed_hash_loop_variant_positive : not tried
[wp] Goal typed_size_ensures : not tried
[wp] Goal typed_size_assert_rte_mem_access : not tried
[wp] Goal typed_size_assigns : not tried
[wp] Goal typed_init_ensures : not tried
[wp] Goal typed_init_ensures_2 : not tried
[wp] Goal typed_init_assert_rte_mem_access : not tried
[wp] Goal typed_init_loop_invariant_preserved : not tried
[wp] Goal typed_init_loop_invariant_established : not tried
[wp] Goal typed_init_loop_invariant_2_preserved : not tried
[wp] Goal typed_init_loop_invariant_2_established : not tried
[wp] Goal typed_init_assert_rte_index_bound : not tried
[wp] Goal typed_init_assert_rte_index_bound_2 : not tried
[wp] Goal typed_init_assert_rte_mem_access_2 : not tried
[wp] Goal typed_init_assert_rte_signed_overflow : not tried
[wp] Goal typed_init_loop_assigns_part1 : trivial
[wp] Goal typed_init_loop_assigns_part2 : not tried
[wp] Goal typed_init_assigns_part1 : not tried
[wp] Goal typed_init_assigns_part2 : not tried
[wp] Goal typed_init_assigns_part3 : not tried
[wp] Goal typed_init_loop_variant_decrease : not tried
[wp] Goal typed_init_loop_variant_positive : not tried
[wp] Goal typed_add_complete_full_nominal : not tried
[wp] Goal typed_add_disjoint_full_nominal : not tried
[wp] Goal typed_add_assert_rte_index_bound : not tried
[wp] Goal typed_add_assert_rte_mem_access : not tried
[wp] Goal typed_add_assert_rte_index_bound_2 : not tried
[wp] Goal typed_add_assert_rte_index_bound_3 : not tried
[wp] Goal typed_add_assert_rte_index_bound_4 : not tried
[wp] Goal typed_add_assert_rte_index_bound_5 : not tried
[wp] Goal typed_add_assert_rte_mem_access_2 : not tried
[wp] Goal typed_add_assert_rte_mem_access_3 : not tried
[wp] Goal typed_add_assert_rte_index_bound_6 : not tried
[wp] Goal typed_add_assert_rte_mem_access_4 : not tried
[wp] Goal typed_add_assert_rte_mem_access_5 : not tried
[wp] Goal typed_add_assert_rte_signed_overflow : not tried
[wp] Goal typed_add_assert_rte_mem_access_6 : not tried
[wp] Goal typed_add_assert_rte_mem_access_7 : not tried
[wp] Goal typed_add_assert_rte_signed_overflow_2 : not tried
[wp] Goal typed_add_assigns_exit : trivial
[wp] Goal typed_add_assigns_normal_part1 : trivial
[wp] Goal typed_add_assigns_normal_part2 : not tried
[wp] Goal typed_add_assigns_normal_part3 : not tried
[wp] Goal typed_add_assigns_normal_part4 : not tried
[wp] Goal typed_add_assigns_normal_part5 : not tried
[wp] Goal typed_add_assigns_normal_part6 : not tried
[wp] Goal typed_add_assigns_normal_part7 : not tried
[wp] Goal typed_add_assigns_normal_part8 : not tried
[wp] Goal typed_add_assigns_normal_part9 : not tried
[wp] Goal typed_add_call_hash_requires : not tried
[wp] Goal typed_add_nominal_ensures : not tried
[wp] Goal typed_add_nominal_ensures_2 : not tried
[wp] Goal typed_add_nominal_ensures_3 : not tried
[wp] Goal typed_add_nominal_ensures_4 : not tried
[wp] Goal typed_add_nominal_ensures_5 : not tried
[wp] Goal typed_add_nominal_assigns_exit : trivial
[wp] Goal typed_add_nominal_assigns_normal_part1 : trivial
[wp] Goal typed_add_nominal_assigns_normal_part2 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part3 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part4 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part5 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part6 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part7 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part8 : not tried
[wp] Goal typed_add_nominal_assigns_normal_part9 : not tried
[wp] Goal typed_add_full_ensures : not tried
[wp] Goal typed_add_full_assigns_exit : trivial
[wp] Goal typed_add_full_assigns_normal_part1 : trivial
[wp] Goal typed_add_full_assigns_normal_part2 : not tried
[wp] Goal typed_add_full_assigns_normal_part3 : not tried
[wp] Goal typed_add_full_assigns_normal_part4 : not tried
[wp] Goal typed_add_full_assigns_normal_part5 : not tried
[wp] Goal typed_add_full_assigns_normal_part6 : not tried
[wp] Goal typed_add_full_assigns_normal_part7 : not tried
[wp] Goal typed_add_full_assigns_normal_part8 : not tried
[wp] Goal typed_add_full_assigns_normal_part9 : not tried
[wp] Goal typed_mem_binding_complete_found_not_found : not tried
[wp] Goal typed_mem_binding_disjoint_found_not_found : not tried
[wp] Goal typed_mem_binding_loop_invariant_preserved : not tried
[wp] Goal typed_mem_binding_loop_invariant_established : not tried
[wp] Goal typed_mem_binding_loop_invariant_2_preserved : not tried
[wp] Goal typed_mem_binding_loop_invariant_2_established : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_2 : not tried
[wp] Goal typed_mem_binding_assert_rte_mem_access : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_3 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_4 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_5 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_6 : not tried
[wp] Goal typed_mem_binding_assert_rte_mem_access_2 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_7 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_8 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_9 : not tried
[wp] Goal typed_mem_binding_assert_rte_index_bound_10 : not tried
[wp] Goal typed_mem_binding_assert_rte_mem_access_3 : not tried
[wp] Goal typed_mem_binding_assert_rte_signed_overflow : not tried
[wp] Goal typed_mem_binding_loop_assigns_part1 : trivial
[wp] Goal typed_mem_binding_loop_assigns_part2 : not tried
[wp] Goal typed_mem_binding_assigns_exit_part1 : trivial
[wp] Goal typed_mem_binding_assigns_exit_part2 : not tried
[wp] Goal typed_mem_binding_assigns_exit_part3 : not tried
[wp] Goal typed_mem_binding_assigns_exit_part4 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part1 : trivial
[wp] Goal typed_mem_binding_assigns_normal_part2 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part3 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part4 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part5 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part6 : not tried
[wp] Goal typed_mem_binding_assigns_normal_part7 : not tried
[wp] Goal typed_mem_binding_loop_variant_decrease : not tried
[wp] Goal typed_mem_binding_loop_variant_positive : not tried
[wp] Goal typed_mem_binding_call_hash_requires : not tried
[wp] Goal typed_mem_binding_call_eq_string_requires : not tried
[wp] Goal typed_mem_binding_call_eq_string_requires_2 : not tried
[wp] Goal typed_mem_binding_found_ensures : not tried
[wp] Goal typed_mem_binding_not_found_ensures : not tried
src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle deleted 100644 → 0
+ 0
− 19
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing loop-statement.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Goal typed_lemma_Lb : not tried
[wp] Goal typed_loop_statement_requires_Scond : not tried
[wp] Goal typed_loop_statement_ensures_Sbody : not tried
[wp] Goal typed_loop_statement_assigns : trivial
[wp] Goal typed_loop_statement_requires_Rinv : not tried
[wp] Goal typed_loop_statement_ensures_Scond : not tried
[wp] Goal typed_loop_statement_ensures_Sloop : not tried
[wp] Goal typed_loop_statement_loop_invariant_Iloop_preserved : not tried
[wp] Goal typed_loop_statement_loop_invariant_Iloop_established : not tried
[wp] Goal typed_loop_statement_loop_assigns_part1 : trivial
[wp] Goal typed_loop_statement_loop_assigns_part2 : not tried
[wp] Goal typed_loop_statement_assigns_2_exit_part1 : trivial
[wp] Goal typed_loop_statement_assigns_2_exit_part2 : not tried
[wp] Goal typed_loop_statement_assigns_2_normal_part1 : trivial
[wp] Goal typed_loop_statement_assigns_2_normal_part2 : not tried
src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle deleted 100644 → 0
+ 0
− 181
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing frama_c_hashtbl_solved.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 102 goals scheduled
[wp] [Qed] Goal typed_eq_string_complete_eq_not_eq : Valid
[wp] [Qed] Goal typed_eq_string_disjoint_eq_not_eq : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_eq_string_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_eq_string_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_eq_string_loop_assigns : Valid
[wp] [Qed] Goal typed_eq_string_assigns_part1 : Valid
[wp] [Qed] Goal typed_eq_string_assigns_part2 : Valid
[wp] [Qed] Goal typed_eq_string_assigns_part3 : Valid
[wp] [Qed] Goal typed_eq_string_assigns_part4 : Valid
[wp] [Qed] Goal typed_eq_string_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_eq_string_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_eq_ensures : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_not_eq_ensures : Valid
[wp] [Alt-Ergo] Goal typed_hash_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_hash_loop_invariant_established : Valid
[wp] [Qed] Goal typed_hash_loop_assigns : Valid
[wp] [Qed] Goal typed_hash_assigns_part1 : Valid
[wp] [Qed] Goal typed_hash_assigns_part2 : Valid
[wp] [Qed] Goal typed_hash_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_hash_loop_variant_positive : Valid
[wp] [Qed] Goal typed_size_ensures : Valid
[wp] [Qed] Goal typed_size_assigns : Valid
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_assigns_part2 : Valid
[wp] [Script] Goal typed_init_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
[wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
[wp] [Qed] Goal typed_add_assigns_exit : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part5 : Valid
[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part6 : Valid
[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part7 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part8 : Valid
[wp] [Qed] Goal typed_add_assigns_normal_part9 : Valid
[wp] [Qed] Goal typed_add_call_hash_requires : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_ensures : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_3 : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_4 : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_5 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_exit : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part5 : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part6 : Valid
[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part7 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part8 : Valid
[wp] [Qed] Goal typed_add_nominal_assigns_normal_part9 : Valid
[wp] [Alt-Ergo] Goal typed_add_full_ensures : Valid
[wp] [Qed] Goal typed_add_full_assigns_exit : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part5 : Valid
[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part6 : Valid
[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part7 : Valid
[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part8 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part9 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_complete_found_not_found : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_disjoint_found_not_found : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_preserved : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_mem_binding_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_mem_binding_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_mem_binding_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_exit_part4 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part5 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part6 : Valid
[wp] [Qed] Goal typed_mem_binding_assigns_normal_part7 : Valid
[wp] [Qed] Goal typed_mem_binding_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_mem_binding_loop_variant_positive : Valid
[wp] [Qed] Goal typed_mem_binding_call_hash_requires : Valid
[wp] [Qed] Goal typed_mem_binding_call_eq_string_requires : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_call_eq_string_requires_2 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_found_ensures : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_not_found_ensures : Valid
[wp] Proved goals: 102 / 102
Qed: 69
Script: 1
Alt-Ergo: 32
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
eq_string 11 4 15 100%
hash 6 1 7 100%
size 2 - 2 100%
init 8 4 13 100%
add 24 15 39 100%
mem_binding 18 8 26 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function add
[rte] annotating function eq_string
[rte] annotating function hash
[rte] annotating function init
[rte] annotating function mem_binding
[rte] annotating function size
[wp] 41 goals scheduled
[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access_2 : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_hash_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_hash_assert_rte_mem_access_2 : Valid
[wp] [Alt-Ergo] Goal typed_hash_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_size_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_init_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_init_assert_rte_index_bound_2 : Valid
[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access_2 : Valid
[wp] [Alt-Ergo] Goal typed_init_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_add_assert_rte_index_bound_2 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound_3 : Valid
[wp] [Qed] Goal typed_add_assert_rte_index_bound_4 : Valid
[wp] [Qed] Goal typed_add_assert_rte_index_bound_5 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_add_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_add_assert_rte_index_bound_6 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_add_assert_rte_mem_access_5 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_6 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_7 : Valid
[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow_2 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_2 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_3 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_4 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_5 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_6 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_7 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_8 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_9 : Valid
[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_10 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_3 : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_signed_overflow : Valid
[wp] Proved goals: 41 / 41
Qed: 16
Alt-Ergo: 25
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
eq_string 11 7 18 100%
hash 7 3 10 100%
size 2 1 3 100%
init 10 7 18 100%
add 30 24 54 100%
mem_binding 25 15 40 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle deleted 100644 → 0
+ 0
− 30
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing loop-statement.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_Lb : Unsuccess
[wp] [Qed] Goal typed_loop_statement_requires_Scond : Valid
[wp] [Qed] Goal typed_loop_statement_ensures_Sbody : Valid
[wp] [Qed] Goal typed_loop_statement_assigns : Valid
[wp] [Alt-Ergo] Goal typed_loop_statement_requires_Rinv : Valid
[wp] [Qed] Goal typed_loop_statement_ensures_Scond : Valid
[wp] [Qed] Goal typed_loop_statement_ensures_Sloop : Valid
[wp] [Alt-Ergo] Goal typed_loop_statement_loop_invariant_Iloop_preserved : Valid
[wp] [Alt-Ergo] Goal typed_loop_statement_loop_invariant_Iloop_established : Valid
[wp] [Qed] Goal typed_loop_statement_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_loop_statement_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_exit_part1 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_exit_part2 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part1 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part2 : Valid
[wp] Proved goals: 14 / 15
Qed: 11
Alt-Ergo: 3 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Ploop - - 1 0.0%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
loop_statement 11 3 14 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle deleted 100644 → 0
+ 0
− 254
View file @ 82bea003
# frama-c -wp [...]
[kernel] Parsing alias_assigns_hypotheses.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function comprehension_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 85) in 'comprehension_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 86) in 'comprehension_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 84) in 'comprehension_alias':
Effect at line 88
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function field_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 54) in 'field_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 55) in 'field_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 53) in 'field_alias':
Effect at line 57
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function field_range_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 66) in 'field_range_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 67) in 'field_range_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 65) in 'field_range_alias':
Effect at line 69
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 25) in 'formal_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 26) in 'formal_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 24) in 'formal_alias':
Effect at line 28
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_alias_array
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 40) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 41) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 42) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (1/2):
Effect at line 44
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (2/2):
Effect at line 45
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_no_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 33) in 'formal_no_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 32) in 'formal_no_alias':
Effect at line 35
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function global_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 10) in 'global_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 11) in 'global_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 9) in 'global_alias':
Effect at line 13
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function global_no_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 18) in 'global_no_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 17) in 'global_no_alias':
Effect at line 20
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function set_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 74) in 'set_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 75) in 'set_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 73) in 'set_alias':
Effect at line 77
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function union_alias
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 95) in 'union_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file alias_assigns_hypotheses.i, line 96) in 'union_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file alias_assigns_hypotheses.i, line 94) in 'union_alias':
Effect at line 98
Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
requires \separated(g_alias,\union(&g_alias,global+(..)));
*/
void global_alias(void);
[wp] Warning: Memory model hypotheses for function 'global_no_alias':
/*@ behavior typed: requires \separated(g_alias,&g_alias); */
void global_no_alias(void);
[wp] Warning: Memory model hypotheses for function 'formal_alias':
/*@
behavior typed:
requires \separated(global+(..),f_alias);
requires \separated(f_alias,global+(..));
*/
void formal_alias(int *f_alias);
[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
/*@
behavior typed:
requires \separated(global+(..),alias_array+(..));
requires \separated(&(*alias_array)[0 .. 1],global+(..));
*/
void formal_alias_array(int (*alias_array)[2]);
[wp] Warning: Memory model hypotheses for function 'field_alias':
/*@
behavior typed:
requires \separated(global+(..),x);
requires \separated(&x->x,global+(..));
*/
void field_alias(struct X *x);
[wp] Warning: Memory model hypotheses for function 'field_range_alias':
/*@
behavior typed:
requires \separated(global+(..),x+(..));
requires \separated(&(x + (0 .. 3))->x,global+(..));
*/
void field_range_alias(struct X *x);
[wp] Warning: Memory model hypotheses for function 'set_alias':
/*@
behavior typed:
requires \separated(\union(global+(..),&g_alias),f_alias);
requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
*/
void set_alias(int *f_alias);
[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
/*@
behavior typed:
requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
\union(&g_alias,global+(..)));
*/
void comprehension_alias(void);
[wp] Warning: Memory model hypotheses for function 'union_alias':
/*@
behavior typed:
requires \separated(\union(global+(..),&g_alias),f_alias);
requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
*/
void union_alias(int *f_alias);
src/plugins/wp/tests/wp_manual/dune 0 → 100644
+ 3
− 0
View file @ 834c4a23
(subdir
result_qualif/working_dir
(copy_files ../../working_dir/*))
src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
+ 1
− 1
View file @ 834c4a23
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
*/ */
/* run.config_qualif /* run.config_qualif
DEPS: @WP_SESSION@/script/*
OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@ OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/ */
......
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