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

[wp/tests] restore run.config_qualif for a test

parent 30e29676
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 @ 71cb033c
/* run.config
OPT: -wp-model Typed+cast
*//* run.config_qualif
*/
/* run.config_qualif
OPT: -wp -wp-model Typed+cast -wp-steps 50
*/
// Test logic types defined from C types
//--------------------------------------
typedef struct { int x ; int y ; } Point ;
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+ 27
− 27
View file @ 71cb033c
# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
# frama-c -wp -wp-model 'Typed (Cast)' -wp-timeout 90 -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
......@@ -41,34 +41,34 @@
[wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
[wp] [Alt-Ergo] Goal typed_h_ensures : Unsuccess (Stronger)
[wp] [Qed] Goal typed_h_assigns_exit : Valid
[wp] [Qed] Goal typed_h_assigns_normal : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_8 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_9 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_10 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_11 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_12 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_13 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_14 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_15 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
[wp] Proved goals: 5 / 21
Qed: 3
Alt-Ergo: 2 (unsuccess: 16)
[wp] [Qed] Goal typed_cast_h_ensures : Valid
[wp] [Qed] Goal typed_cast_h_assigns_exit : Valid
[wp] [Qed] Goal typed_cast_h_assigns_normal : Valid
[wp] [Qed] Goal typed_cast_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_4 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_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_cast_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_cast_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_cast_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_cast_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_cast_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_cast_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_18 : Unsuccess (Stronger)
[wp] Proved goals: 4 / 21
Qed: 4
Alt-Ergo: 0 (unsuccess: 17)
[wp] Report in: 'tests/wp_acsl/oracle_qualif/logic.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/logic.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
h 2 - 3 66.7%
main 1 2 (56..80) 18 16.7%
h 3 - 3 100%
main 1 - 18 5.6%
-------------------------------------------------------------
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