From a3b0eda2778fdcf4a5f97029910b5dcdd2f00a52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Wed, 11 Sep 2019 14:31:03 +0200 Subject: [PATCH] [wp/cache] update oracles (time limit only, on result change) --- src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle | 2 +- .../wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle | 2 +- .../wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle | 2 +- src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle | 2 +- src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle | 2 +- src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle | 2 +- src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle | 2 +- src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle | 2 +- .../tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle | 2 +- .../wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle | 2 +- src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle | 2 +- .../wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle | 2 +- .../wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle | 2 +- src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle | 2 +- .../wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle | 2 +- .../binary-multiplication-without-overflow.res.oracle | 2 +- .../wp_gallery/oracle_qualif/binary-multiplication.res.oracle | 2 +- .../wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle | 2 +- .../wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle | 2 +- .../wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle | 2 +- .../oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle | 2 +- .../oracle_qualif/frama_c_exo3_solved.simplified.res.oracle | 2 +- .../wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle | 2 +- .../wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle | 2 +- src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle | 2 +- src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle | 2 +- src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle | 2 +- src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle | 2 +- src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/reference.res.oracle | 2 +- .../wp_hoare/oracle_qualif/reference_and_struct.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle | 2 +- .../wp_hoare/oracle_qualif/reference_array_simple.res.oracle | 2 +- .../wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle | 2 +- .../wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle | 2 +- .../wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle | 2 +- .../wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle | 2 +- .../tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle | 2 +- src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle | 2 +- .../wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle | 2 +- .../tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle | 2 +- src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle | 2 +- src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle | 2 +- .../wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle | 2 +- .../wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle | 2 +- src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle | 2 +- .../tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle | 2 +- .../tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle | 2 +- .../tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle | 2 +- src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle | 2 +- .../tests/wp_typed/oracle_qualif/struct_array_type.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle | 2 +- src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle | 2 +- src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle | 2 +- src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_string.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle | 2 +- .../wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle | 2 +- src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle | 2 +- .../wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle | 2 +- .../wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle | 2 +- .../wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle | 2 +- 224 files changed, 224 insertions(+), 224 deletions(-) diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle index 1af0a4978ea..29c9c66f579 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/sharing.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle index 13b5a090e32..ee7e3d8c42b 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing) [kernel] tests/wp/stmtcompiler_test.i:136: Warning: Body of function if_assert falls-through. Adding a return statement diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle index 23141b87e96..2867ef1ce9f 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle index 8ef82489efb..e7058249e03 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp/wp_behav.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle index 5f62257e35d..3cd8c9dc87e 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp/wp_behav.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle index da92bd060d1..ef2759505d0 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle index f52504145b9..bdf16d02cb8 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/wp_eqb.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle index 38dfb47769e..e0fba0eeebb 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Hoare' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_strategy.c (with preprocessing) [rte] annotating function bts0513 [rte] annotating function bts0513_bis diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle index 181bf2a9fbc..c423c72e132 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle index 22512c43596..e6f6bea9c68 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle index a532ef8d1cf..26d8e212c80 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle index 36a8e376b74..97318c56ec4 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle index 64c7d444dc0..db587673eac 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle index 64e97d8799e..740d097ec79 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle index 736e31a325f..a3493e03661 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle index 1af5465d131..0ce1be644f7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle index bcb6ca0c309..23321ffd00c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle index 48fb4714a1f..c76035e0829 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle index cf0946ede61..e4be1fdb79c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle index bf4efdc83af..a6187ffba8d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 5 [...] +# frama-c -wp -wp-steps 5 [...] [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle index c4b1a1c2873..cfee3c57e18 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle index b9250d09987..1c0f3f3f388 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle index 0162e0980a3..7ddef8f6c11 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle index 6c52f44f79d..96ac43f8525 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/cnf.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle index 28838da6b6b..98b954ee531 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle index 12959633271..fe8628eb6a8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle index 92c78b1d828..3b1a448537a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle index b0357286139..90d4a24c060 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle index a8ae2141cef..8a4506b88c4 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle index 33fc1d116f1..44350c644f6 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/equal.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle index 221c3d19676..d4667be0f77 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle index bdbccbefae2..c77722b1f2e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle index 9623ee6b44e..c8fc8cbcd72 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle index 9e580ba61f0..b287d5db2dc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle index 8e07203beb3..32404156c7e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle index 8a569a28b30..d448c6b3d8f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle index 519128a270e..46b74f8ec70 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle index 65099e7692b..0185197bcef 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle index cf4c863ff12..5d562543524 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle index f80035a9095..876ff1d2ac0 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle index 8351bc41d14..68a296dd46d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle index e382296ef46..24104211960 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle index b5788d4ee54..f0976611dcc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/null.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle index 7c110cb79df..3638dce1955 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle index 205d8ead9ed..9d969ebd5f4 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle index 5ab98f1194f..de530957855 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle index 627cd3b588e..f834bdff41e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing) [kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning: unexpected token ';' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle index 14de3dc9b99..ccc22350c9f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing) [kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning: unexpected token ';' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle index 8dc5e9a29d3..e4a282e1d29 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle index a5a0d165b2f..23f22eec01d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle index c40c87ec26c..5d02297a0fa 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle index 54d7726924e..9871b438a59 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/record.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle index 1132c478b4b..e5035856288 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/record.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle index 384bd75e155..1ffb95b1d5e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle index 498f74657dc..8c9276a68e7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle index da7fdb385c1..074954472b7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle index 5313181afd3..628c2eb2f84 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle index 12b3d155f8b..8de21842d8f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/tset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle index ddfbb1e2348..66fb81dadf2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle index 09fd140cec8..ca7c410e823 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle index 36e568d169f..9c8efdfa48e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle index 48b1444f5ee..a457770ae98 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle index c8becb7fc24..3eb2f63b434 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle index 384654b8407..d5a3dd35879 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle index 92e03a00f08..f84001a741b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte [...] +# frama-c -wp -wp-rte -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/issue_141.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle index aff0d060520..4be131e6040 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle index 33b4eab1662..6ade8dc8e47 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle index 4282d2c325e..e3c50082e0a 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_bts/bts779.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle index 1215384b9c1..5cd9ede34c1 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_bts/bts788.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle index f28391971bd..360961ac42c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/bts986.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle index 374c06fec66..4de546639bd 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle index 6a39dfa841d..746589ddd94 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle index 61ff3d4d143..710eb3051e1 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_bts/bts_1360.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle index d45f3ec09d3..eb31be8a44f 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle index 722fea99154..ce7b8a4fe68 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle index d3080fe8235..55913b62c70 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle index d121feba836..eeccda7e270 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle index cccf36bcb81..99bc35317b0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle index 7855fdce2b6..8434a188aab 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle index 1c2fe17584e..4d4b554f999 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle index 40b78670f5e..d4b8e198b08 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle index 79511ba1720..f241129fe79 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle index 9f89e1687a3..e0de6d5f1e0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle index 4231e564c8c..42d8ba9e5b7 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle index 341cbfc3a20..e3ee19b027b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle index 5809812ed68..6985b4d2e2f 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle index 020e138a0e7..feee3c91099 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle index 740bb8ea13f..e9bc0c7109c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle index 377e3ee717a..f391d02b573 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle index 06085822d33..f9611321b0c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle index 5c91074b9d1..a1ec9480bb7 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle index cf0252e05e8..592d4a5f613 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle index 62d996fcf99..565ebf75c77 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle index f5969a63fa8..bfdf15d4931 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle index b12a5179d4c..4aa305f3c58 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -warn-unsigned-overflow [...] +# frama-c -wp -warn-unsigned-overflow [...] [kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle index 8bb2f2aa48e..42de806ba95 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...] +# frama-c -wp -wp-timeout 90 [...] [kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle index 650002bfa46..3d750b31c69 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle index c0bfb08ca3b..deaba47c54d 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle index dc1ca6605e8..c74a9513362 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle index d28a3f0f2f2..4476cb8738d 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.v2.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle index 86b8662c591..5c40a1cfb36 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle index a89aa37dc9e..a551c80874c 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle index 725c0969604..5f587e1a5d0 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle index 26633fe4465..185df39d3ab 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle index 90e3b2a6580..a4876a5fd53 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle index 8988bb2d21b..82582e12b00 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/dispatch_var.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle index 585e9038dc7..16765c955e3 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let [...] [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle index 750611233e6..5757c0013bd 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle index f4bbe476b3e..435a2090821 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/isHoare.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle index 4a3a8203b8c..ab5a5a62ec3 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle index 06c19d356c8..084f416c0a5 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/logicref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle index 11f09dc4fe7..8a276ac051f 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/logicref_simple.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle index 974bff5d6c4..604da725396 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle index dba3f12ed28..8980ef3f8b5 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_and_struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle index 19d23d63579..9ccbcce0d1f 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle index c4971ab52e2..78b38ba1195 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_array_simple.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle index 1bef150b691..4f3725c5bb2 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/refguards.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle index df1f35bd569..a4c3d2bc111 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_manual/manual.i (no preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap1.h (with preprocessing) diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle index 39ecdb3048a..5897a7cede1 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_manual/manual.i (no preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap2.h (with preprocessing) diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle index 83a1077be56..cad3da72c7d 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [rte] annotating function swap ------------------------------------------------------------- Functions WP Alt-Ergo Total Success diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle index 3be28fd7c30..266bc967362 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle index bee639e5bed..4b9063d0f17 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle index 5ff11df2299..c56a75a74f2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle index 4737abaddaf..b7c278753cf 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/asm.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle index 40432fecac9..93c9d28b232 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle index 7edd3815e32..cf4825d1b68 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-no-let [...] [kernel] Parsing tests/wp_plugin/bool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle index e58dd159662..d663290a72f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/copy.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle index 3a2e135ecde..7fdb8a52676 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle index b60e1d430a6..424e076b606 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle index c711d65adab..29dde40a08d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle index 1712b1e0c18..803faf1078b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle index 3e525c78036..8f2da577ae2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle index dff0921f02e..9f87d54d4ed 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle index 1aef24e167a..2230d173868 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle index 31633324320..00476c270d8 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning: Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle index 43d07c8326c..82e75838138 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed' [...] [kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning: Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle index 773b4122b04..8247a946f24 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/frame.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle index 4341a8387fa..f5f790a0cff 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle index e58fc4777e8..58f1a2f1d92 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 240 -wp-steps 1500 [...] +# frama-c -wp -wp-timeout 240 [...] [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle index f719ce191c9..bc0a1b82ce3 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle index 74fbe626590..c2c2e3ceccb 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle index 8fee97c8110..1538d48fe05 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing) [kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing) [wp] Running WP plugin... diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle index 9a9e1245748..c303e914f2a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle index 06ab6be80f4..3e092c05173 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle index 09a14411797..21e508fd591 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle index 8e07c7e3030..b4667f759fa 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle index c73a0cad6ce..84704dba34e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loop.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle index 887d7f68708..1243a954f85 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle index 190504de364..73078e24dae 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle index be03eb0c545..61bff7f94a5 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle index 80f261630b6..85ae2cc2fcd 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/mask.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle index 7af20aa4633..fb561d0e65e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle index 51b0b773d0d..6117c36a1ed 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle index 9fbeaeadf91..e643d4c567d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle index e86cc65ef01..e4b76ba8669 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle index 0815def0020..c243d5abbdc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle index f3b60ab0089..9fed766a89f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle index 75b57c96bb5..b8758ed7581 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle index 472834ac035..281d6f5ec59 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/params.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle index d77ba62ed0b..cda0cfc000b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/plet.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle index 001d2294e71..aa3a09060e6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/polarity.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle index 5caef16184f..bbe0916d104 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle index 3a7456bff6c..eb995af1813 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle index ac262be9081..417ba94b1f0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle index c2817aedca9..555a56a8bda 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle index 60d453b63fc..23a0acbb4ed 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle index c637752ab86..4c1eec778b0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle index a27557f5d76..5db0c6c63cd 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle index 13f3d7def48..e1033c3097e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle index fdcbde23308..e372635af12 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/struct_hack.i (no preprocessing) [kernel] tests/wp_plugin/struct_hack.i:46: Warning: parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle index 87dc894abd2..b9adc007794 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle index 26b6ff968ac..6c887c02728 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle index acc077c4877..e53872ad04a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/trig.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle index bf1a7e953c7..c077b5a44c1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle index 81ae9d616c3..61a5c555291 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle index 65756a3d261..42aeee4e9a9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle index 8fa3b75a019..bd4a0fcd4ac 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle index 486277148c2..688dc734ded 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle index 4a6c59025d9..df7d9928519 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/natural.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle index 4f2da7d3351..308c618c46d 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle index 244af382e05..359493b38c2 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle index 162e249c284..02c96c873c8 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle index 4ebd433885c..a189a671dc8 100644 --- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle +++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle index d71cbec20ec..bad51ba3f9b 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing) [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle index 407f88f1e8d..1c4aad2918c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing) [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle index 882fd42aa67..a8932bccedf 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/avar.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle index 68e665c137e..de595eb7883 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle index a64bd492a48..7c6f289582e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle index 8549fbcc64f..fc0bebfe6e6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle index e8a1ae26e73..33c30e5011f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle index d0235b8a087..44d2660eb21 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle index 9a11fc16b0c..84f7b84effb 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle index 1c1f801a70c..f89e7bf6498 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle index eb02a84c8a1..d9dd667a563 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle index 92b3928c5f7..32cabdf891b 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle index 27195d8e897..4c071c988dc 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle index a636e612e81..2b61ac101b7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed' [...] [kernel] Parsing tests/wp_typed/unit_float.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_typed/unit_float.i:21: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle index 5aab1b03622..b5a6c46d069 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle index 2f4749d9608..176778cfcb4 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle index f83f7c8a483..6ff11cc1d5c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle index 34fd709d63e..187ce058196 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle index 4a7acb218e3..8ee86f60111 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle index 907467024d1..f0b944bdbcc 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Raw)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Raw)' [...] [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle index bf3d6522ac9..28cab47713a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle index 41ceb697fd2..514db21cf01 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle index 52238385668..b4416b982a1 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle index a8a5e99ca4c..05965e3ea99 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle index b9b2d0e9c26..2a0fe19ec72 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle index d26be5ba50b..5408bc35bad 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle index d63ff2f336b..edcc63f6306 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle index 0322e3c7950..4aaf43770a3 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle index 549deb2265c..f6b7811bc5a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle index 0a25b0620ac..2bec0646b50 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle index 18f10ef164a..5d0066fd74e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 300 [...] +# frama-c -wp -wp-steps 300 [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle index c2358598c8d..c8197b04ff7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle index 347c74e839d..aefa32d0a90 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle index 004a6b35b20..b3cc0003566 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle index 68f3ed824c6..0689081a4c3 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_string.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle index 260b1c3252f..a8f54d19ca9 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle index bf1b70d2492..7b634d39838 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle index 0d5c1cdfb0c..4993df34f43 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_usage/caveat2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle index c210cf13b65..5b69c867545 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_usage/caveat_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle index f85eb21dbee..b0661cf0328 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle index d5147644f0c..da52504bdeb 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' -- GitLab