Commit d18e2c19 authored by François Bobot's avatar François Bobot
Browse files

Merge branch 'feature/wp/remove-test-log' into 'master'

[wp/tests] suppress range-steps report

See merge request frama-c/frama-c!2436
parents 574af106 93fff3f8
......@@ -1216,12 +1216,14 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
let name = "Wp.Cache.mode"
let compile () =
try
if not (Wp_parameters.CacheEnv.get()) then
raise Not_found ;
let origin = "FRAMAC_WP_CACHE" in
parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
with Not_found ->
try
parse_mode ~origin:"-wp-cache" ~fallback:"none"
(Wp_parameters.Cache.get())
let mode = Wp_parameters.Cache.get() in
parse_mode ~origin:"-wp-cache" ~fallback:"none" mode
with Not_found ->
if Wp_parameters.has_session ()
then Update else NoCache
......
{ "wp:global": { "script": { "total": 5, "valid": 4, "unknown": 1 },
"wp:main": { "total": 5, "valid": 4, "unknown": 1 } },
"wp:axiomatics": { "A": { "lemma_Hyp_Forall_Or_bis": { "script": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"lemma_Hyp_Forall_And": { "script": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"lemma_Goal_Exist_Or": { "script": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"lemma_Goal_Exist_And_bis": { "script": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"lemma_Goal_Exist_And": { "script": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "script": { "total": 5,
"valid": 4,
"unknown": 1 },
"wp:main": { "total": 5,
"valid": 4,
"unknown": 1 } } } } }
@CONSOLE
@ZERO " - "
@ZERO " -"
@HEAD
@CHAPTER
-------------------------------------------------------------
%chapter &18: WP &26: Alt-Ergo &42: Total &51:Success
------------------------------------------------------------
%chapter &25: WP &34:Alt-Ergo &43: Total &52:Success
@SECTION
%name &18:%wp &24: %{Alt-Ergo,2.0.0,} %range &42:%total &51: %success%%
%name &25:%wp &34:%{Alt-Ergo,2.0.0,} &43:%total &52: %success%%
@TAIL
-------------------------------------------------------------
------------------------------------------------------------
@END
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@
OPT:
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 8 },
"wp:main": { "total": 1, "valid": 1, "rank": 8 } },
"wp:functions": { "f": { "f_ensures": { "why3:Alt-Ergo,2.0.0": { "total": 1,
"valid": 1,
"rank": 8 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 8 } },
"wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
"valid": 1,
"rank": 8 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 8 } } } } }
{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 13 },
"wp:main": { "total": 1, "valid": 1, "rank": 13 } },
"wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 13 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 13 } },
"wp:section": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 13 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 13 } } } } }
......@@ -8,9 +8,7 @@
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo 2.0.0: 1
[wp] Report in: 'tests/wp/oracle_qualif/sharing.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/sharing.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f - 1 (28..40) 1 100%
-------------------------------------------------------------
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f - 1 1 100%
------------------------------------------------------------
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 9, "valid": 1,
"unknown": 8, "rank": 2 },
"qed": { "total": 18, "valid": 18 },
"wp:main": { "total": 27, "valid": 19, "unknown": 8,
"rank": 2 } },
"wp:functions": { "empty": { "empty_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_assign": { "one_assign_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_if": { "one_if_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"some_seq": { "some_seq_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"some_seq_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } },
"main_ensures_result": { "main_ensures_result_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } } },
"main": { "main_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"not_main": { "not_main_assert_bad": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"main_assigns_global": { "main_assigns_global_assert_bad":
{ "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"main_assigns_global_assert_2":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"main_assigns_global_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 2,
"valid": 2 },
"wp:main":
{ "total": 3,
"valid": 2,
"unknown": 1 } } },
"zloop": { "zloop_assert_bad": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_3": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_loop_invariant": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
"valid": 1,
"unknown": 1 } },
"zloop_ensures": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 3, "unknown": 3 },
"qed": { "total": 4,
"valid": 4 },
"wp:main": { "total": 7,
"valid": 4,
"unknown": 3 } } },
"behavior2": { "behavior2_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior3": { "behavior3_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior4": { "behavior4_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior5": { "behavior5_assert_bad": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"if_assert": { "if_assert_assert_missing_return":
{ "why3:Alt-Ergo,2.0.0": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"if_assert_assert_3": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"if_assert_assert_2": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"if_assert_assert": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"valid": 1,
"rank": 2 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 2 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 3,
"valid": 1,
"unknown": 2,
"rank": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 4,
"valid": 2,
"unknown": 2,
"rank": 2 } } },
"compare": { "compare_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } } } }
{ "wp:global": { "alt-ergo": { "total": 9, "valid": 1, "unknown": 8,
"rank": 2 },
"qed": { "total": 18, "valid": 18 },
"wp:main": { "total": 27, "valid": 19, "unknown": 8,
"rank": 2 } },
"wp:functions": { "empty": { "empty_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_assign": { "one_assign_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_if": { "one_if_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"some_seq": { "some_seq_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"some_seq_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } },
"main_ensures_result": { "main_ensures_result_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } } },
"main": { "main_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"not_main": { "not_main_assert_bad": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"main_assigns_global": { "main_assigns_global_assert_bad":
{ "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"main_assigns_global_assert_2":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"main_assigns_global_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 2,
"valid": 2 },
"wp:main":
{ "total": 3,
"valid": 2,
"unknown": 1 } } },
"zloop": { "zloop_assert_bad": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_3": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_loop_invariant": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
"valid": 1,
"unknown": 1 } },
"zloop_ensures": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "alt-ergo": { "total": 3,
"unknown": 3 },
"qed": { "total": 4,
"valid": 4 },
"wp:main": { "total": 7,
"valid": 4,
"unknown": 3 } } },
"behavior2": { "behavior2_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior3": { "behavior3_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior4": { "behavior4_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior5": { "behavior5_assert_bad": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"if_assert": { "if_assert_assert_missing_return":
{ "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"if_assert_assert_3": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"if_assert_assert_2": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"if_assert_assert": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 2 } },
"wp:section": { "alt-ergo": { "total": 3,
"valid": 1,
"unknown": 2,
"rank": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 4,
"valid": 2,
"unknown": 2,