From 18990fcaa0930fe695a120d58e902630837b8f86 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 18 Sep 2020 11:04:43 +0200 Subject: [PATCH] [tests-wp] update oracles following message change --- src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/sharing.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle | 1 - src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle | 1 - .../wp_acsl/oracle/assigned_initialized_memtyped.res.oracle | 1 - .../tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle | 1 - .../wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle | 1 - .../wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/generalized_checks.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/predicates_functions.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle | 1 - src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle | 1 - .../wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle | 1 - src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle | 1 - .../oracle/binary-multiplication-without-overflow.res.oracle | 1 - .../wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle | 1 - src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle | 1 - .../wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle | 1 - .../wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle | 1 - .../tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle | 1 - .../wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle | 1 - .../wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle | 1 - .../wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle | 1 - src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle | 1 - .../tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle | 1 - .../tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle | 1 - .../wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle | 1 - .../wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle | 1 - src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle | 1 - .../wp/tests/wp_plugin/oracle/init_const_guard.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle | 1 - .../wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle | 1 - .../wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle | 1 - src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle | 1 - src/plugins/wp/tests/wp_store/oracle/array.res.oracle | 1 - src/plugins/wp/tests/wp_store/oracle/natural.res.oracle | 1 - src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle | 1 - src/plugins/wp/tests/wp_store/oracle/struct.res.oracle | 1 - src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle | 1 - .../wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle | 1 - .../wp/tests/wp_typed/oracle/array_initialized.0.res.oracle | 1 - .../wp/tests/wp_typed/oracle/array_initialized.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle | 1 - .../wp/tests/wp_typed/oracle/struct_array_type.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle | 1 - src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle | 1 - src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res | 1 - src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle | 1 - 309 files changed, 309 deletions(-) diff --git a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle index 5d27599429e..8e96b463d84 100644 --- a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp/bug_rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function bug ------------------------------------------------------------ Function bug diff --git a/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle index fde404cb14e..e3e370f250f 100644 --- a/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/cfg_loop.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function loop_continue diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle index 6a9b973a8bd..1a343c63052 100644 --- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/sharing.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 1 goal scheduled --------------------------------------------- diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle index bf984a624a7..d7c91e8c587 100644 --- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp/stmtcompiler_test.i:136: Warning: Body of function if_assert falls-through. Adding a return statement [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp/stmtcompiler_test.i:145: Warning: No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle index fbd89c4d7c4..06fb66f8e03 100644 --- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function empty diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle index 5db0bbd2e08..5d027100e99 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/wp_behav.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] tests/wp/wp_behav.c:172: Warning: Ignored specification 'for b1' (generalize to all behavior) [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle index 9c8ae39d657..c28768d2976 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/wp_behavior.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function behaviors diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle index a1618f68266..e6e7eac38d3 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/wp_behavior.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function behaviors diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle index 653c11e9d55..308fadbaa31 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp/wp_call_pre.c:53: Warning: No code nor implicit assigns clause for function g, generating default assigns from the prototype [kernel] tests/wp/wp_call_pre.c:53: Warning: diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle index a11eb1bd135..c8d77c93481 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp/wp_call_pre.c:53: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle index 90c952b11ab..330ae3ce02f 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp/wp_call_pre.c:53: Warning: No code nor implicit assigns clause for function g, generating default assigns from the prototype [kernel] tests/wp/wp_call_pre.c:53: Warning: diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle index e2054c41737..29adcc554a5 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp/wp_call_pre.c:53: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle index 42f82c47985..2b2fcb498fc 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards Goal Pre-condition 'qed_ok,Rstmt' at instruction (file tests/wp/wp_call_pre.c, line 47): diff --git a/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle index 909dc7f4acb..2ab50ab1a47 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/wp_eqb.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp:print-generated] diff --git a/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle index f9a46f91a87..db0e3c425b6 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_strategy.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bts0513 diff --git a/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle index 0613c6137dc..b3d21c9f32f 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp/wp_strategy.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function default_behaviors with behavior default_for_stmt_54 diff --git a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle index e086a73e2e0..219463ff468 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle index a358aef50a3..c7024e87f06 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function jobA diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle index 0e876ef057d..97405e3f050 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function array diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle index ee074a6bd82..a4e3a95a841 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function array diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle index 3e39ff665df..ebcccafc2c7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function array diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle index 34ed9b45a88..ac2da1bad2c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function array diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle index 0c4bd8dfbdf..b8ebbadea5e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle index 35b9d8777b7..47e610fd265 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_assigns_all diff --git a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle index da37a8a78a0..564b0922bf5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle index 545557ea6d6..436b0b25bcc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle index 70d1558a270..320a3fd9ef4 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function band diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle index 93a098b8218..107c96ad0ad 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job1 diff --git a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle index a3bc5a8c09b..30094770c41 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle index ea971496a84..61274ae7016 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 4 goals scheduled [wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle index bae891952be..795c0dfaafc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle index 6de4c095087..d9362c1ce5c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle index db600bf51f7..38d790b5a4d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle index 72d6142a7ae..8df080b73db 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function function ------------------------------------------------------------ Function function diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle index f066a94e1eb..40c1a5853ba 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function usable_axiom [rte] annotating function usable_lemma [wp] 3 goals scheduled diff --git a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle index 8ce615934da..27e7dccf575 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle index 6a6bd49b1a0..dc62954e6b5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Axiomatic 'Event' ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle index 91eb8c84ada..670b0774270 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle index b6ef93ebb14..ea5fa8f5945 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle index 3a3c58f00c0..a543f1f54a2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/equal.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function simple_array diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle index b43e2d4a815..54ae1cc9e6b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle index d1a648f8189..47c04b9140b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle @@ -5,7 +5,6 @@ [kernel:parser:decimal-float] tests/wp_acsl/float_const.i:19: Warning: Floating-point constant 0.1 is not represented exactly. Will use 0x1.999999999999ap-4. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 8 goals scheduled [wp:print-generated] diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle index 98e419a07ae..2c16374dc4a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_acsl/funvar_inv.i:24: Warning: Can not compare pointers in Empty model diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle index 1e8b67744c3..9ed2d133fee 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle index 6b7463a9cd6..233aa076c4f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Axiomatic 'Th' diff --git a/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle index eb1d9e231e8..42361373eba 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle index a1016679f96..5a0fc4b056c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] 3 goals scheduled --------------------------------------------- --- Context 'typed' Cluster 'Compound' diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle index fa3df7a23c2..d6d7a763dab 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_acsl/init_label.i:27: Warning: No code nor implicit assigns clause for function main, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle index ce62bdd3dcb..c072c17ac8b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-no-let [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function fa1 diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle index ec03acf8c19..9501f9dee9b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-no-let [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function fa1 diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle index 2e42b9e3cb6..c1cd26ad017 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle index 9a56e40c655..c84b034766c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_acsl/init_value_mem.i:24: Warning: Can not load value in Empty model diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle index 391310e752a..10608888723 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function formal diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle index a243863d16a..5a91bd928d6 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function globals diff --git a/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle index 753b578819b..be8e2dc018c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bug diff --git a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle index f1bb59e94b4..a9d75cace6c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle index 69e92d2508b..4fca509b739 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle index 85d318865a1..631003d71ae 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_acsl/logic.i:65: Warning: Cast with incompatible pointers types (source: __anonstruct_Buint_4*) diff --git a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle index d6d7c7ffd7f..c4c9cd16d8a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function copy diff --git a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle index 7d61a351b3e..16ac874aa69 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/null.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle index 76387c61d81..4339266bbaf 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_acsl/pointer.i:50: Warning: Uncomparable locations p_0 and mem:t.(0) diff --git a/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle index 0f84cd85b5c..ea63412d59c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function correct diff --git a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle index 0071a69eb1e..eac17274f26 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle @@ -37,7 +37,6 @@ [kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning: P is not a logic variable. Ignoring code annotation [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bitwise diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle index cc8be9b8f30..666a26c85f5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/predicates_functions.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] 1 goal scheduled [wp:print-generated] theory WP diff --git a/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle index 84774868393..e0054bf13b6 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/range.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function test diff --git a/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle index 3a8f0e7073f..430cdc96add 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle index da2599913d0..43d8c4d3ece 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/record.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle index 42be62e6194..f4bf9c3fb0e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function check_acsl diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle index f7f75c47193..36be29ece00 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle index 671f41e12da..2e93da0b17e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -wp-no-let [...] [kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function foo [wp] 2 goals scheduled --------------------------------------------- diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle index 0c38eb7360b..64f1be48e24 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle index 41bb0db4071..ed60c90f282 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/sum_types.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] 3 goals scheduled --------------------------------------------- --- Context 'typed' Cluster 'A_A' diff --git a/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle index 50ee7b41eb8..60245b69a89 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/tset.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle index 272aafaea49..795eedf06cd 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle index fd300d3519d..9cc603d5697 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function rotate_left diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle index d4de7cfa3f0..ed47c09c4a6 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Axiomatic 'Foo' diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle index daf696e3420..b0b0dba7b56 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_compare.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle index ba6653276cc..0becba4e377 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unsupported_builtin.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_acsl/unsupported_builtin.i:10: Warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle index bb65f617048..c617b1318c2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle index bcd622025b4..fc7dbb75573 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle index 6fe18cd9966..8c6fd6aed1b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f3 diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle index bf5748d6871..0340355af42 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts779.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle index 59fb21a87df..fcb5d4edc86 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle index f0a8fc075ef..f7dbfc4d45a 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts986.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle index 2918c8ef8ab..8e39845f524 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_0896.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle index 0f15882a716..377b3829406 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle index f309987b2d5..b56f41848c0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle index 71741906413..7c44e0c9ee5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle @@ -1,7 +1,6 @@ # 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' [rte] annotating function foo_correct [rte] annotating function foo_wrong ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle index 07498d37853..d59e50a899d 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1382.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_bts/bts_1382.i:18: Warning: Cast with incompatible pointers types (source: sint32*) (target: sint8*) diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle index bbb9f2c50e5..aa5c4e32001 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function local diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle index c2ffd640b72..4020061d0ec 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function compute_bizarre with behavior Bizarre diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle index 00b3e3e05a9..a688528d7bc 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_bts/bts_1588.i:19: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle index 89700347331..a7a44770530 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle index 72a0500b84a..d2d36e4287a 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1647.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle index a7a3e7e5f91..aff5dc75447 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1776.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle index 66651f78d70..640c9952226 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function global_frame diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle index 04d57e17090..5b00c3b48f3 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function global_frame diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle index 69059aeba48..3601e1976dd 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle index 3aaa31af0f6..a59bf702249 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle index b1af7c7da5c..38acae5e6e4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2110.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 2 goals scheduled --------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle index aac7caf8ba1..445eee0ff76 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle index 9669fdaf70d..61491a01bbb 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2201.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle index 961bf498400..9d81968e9e5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2246.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bad diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle index f38cfc4e5fd..550dd7a5454 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2501.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] 2 goals scheduled [wp] 2 goals generated ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle index 694a8eed3ce..5cbab700501 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle index b37af5db7fe..b7b15905eb2 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/ex5.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function dummy diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle index ae3e885d910..cb25cf5612d 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle index 9bf1f55fb10..7a59fcea651 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue-516.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] Warning: No definition for 'to_logic_list' interpreted as reads nothing ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle index 2b2e6c21c2d..cb499212b74 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function inconditional_exit 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 f84001a741b..9dd3dd748e7 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,7 +1,6 @@ # 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' [rte] annotating function f [rte] annotating function main [wp] tests/wp_bts/issue_141.i:18: Warning: diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle index 3995ac6f0b6..e7f427ccd5d 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle index e034a5bf910..f8dc63d5e20 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle index 99a9aed869a..9c1dde973cc 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f1 diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle index 297b4d98186..faaeeb6e2dd 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle index 179be9f834b..69016b5d1ff 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function add diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle index 786b948ba14..d30781324d4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Axiomatic 'LISTS' ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle index 3d37a96e7d7..e41e8f471f5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_bts/issue_715_a.i:6: Warning: No code nor implicit assigns clause for function dummy, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle index 06b261910a5..8c82bc192ba 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_bts/issue_715_b.i:9: Warning: No code nor implicit assigns clause for function dummy, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle index d54cb383836..14535c7cf0c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_751.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function acquire diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle index 81c0ed9a9db..0021dc1ad13 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function LoopCurrent diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle index 3c3d2d46a68..ede0b64f8b9 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function getMax diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle index 65c234448ba..6af1e96a96a 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function issue diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle index d1e95f07802..6505c959c08 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle index f3dbc6f8d16..d832b6f5796 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle index 094d64fd5cc..60c6a834f15 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning: [cfg] Forget exits clause of node <blkIn-stmt:26> [wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning: diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle index f573edafe8d..4a3a4384db1 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -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' [rte] annotating function BinaryMultiplication [wp] Goal typed_lemma_ax1_lack : not tried [wp] Goal typed_lemma_sizeof_ok_ok : trivial diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle index 129465cef77..58d59aef852 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function BinaryMultiplication [wp] Goal typed_lemma_ax1_lack : not tried [wp] Goal typed_lemma_ax2_lack : not tried diff --git a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle index b4f4caaaf02..e0c5b20b99e 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_gallery/find.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function find [rte] annotating function find_ptr [rte] annotating function iter_ptr diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle index 388a5387f67..cdf72d9135a 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function exo1 [wp] Goal typed_exo1_ensures : not tried [wp] Goal typed_exo1_ensures_2 : not tried diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle index 01cfab82cf3..daf1e9d366b 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -no-warn-signed-overflow [...] [kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function max_subarray [wp] Goal typed_max_subarray_ensures : not tried [wp] Goal typed_max_subarray_ensures_2 : not tried diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle index 5976d3b8cb9..e21f8f5fe4b 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -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' [rte] annotating function equal_elements [wp] Goal typed_ref_equal_elements_ensures : not tried [wp] Goal typed_ref_equal_elements_ensures_2 : not tried diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle index ea1e78b5835..0a5004c6765 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -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' [rte] annotating function equal_elements [wp] Goal typed_ref_equal_elements_ensures_v1_good : not tried [wp] Goal typed_ref_equal_elements_ensures_v2_good : not tried diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle index d19091020e7..21850665dd1 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function pair [wp] Goal typed_pair_complete_has_pair_no_pair : trivial [wp] Goal typed_pair_disjoint_has_pair_no_pair : trivial diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle index 064dce264b9..a73f6deff1e 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function add [rte] annotating function eq_string [rte] annotating function hash diff --git a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle index 52b5a0ec02f..128fa9a9dd6 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] Goal typed_lemma_Lb : not tried [wp] Goal typed_loop_statement_ensures_Scond : not tried diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle index 4b800e90173..832baab84eb 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function comprehension_alias diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle index 4eb7ef19181..3da623e2493 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function comprehension_alias diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle index 9ec8bc14a7f..f9c6a96edce 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle index 051a94929b4..54ad8489278 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle index bb48a4672be..d2646994c22 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle @@ -23,7 +23,6 @@ Function call_two_ref: { r0 tmp tmp_0 __retres } Function g: { *pg tmp } Function array_in_struct_param: { sf } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function array_in_struct_param diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle index 72989020ece..8c876f6db38 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_global diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle index 181d3c1dad2..44ae58e7b74 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_global diff --git a/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle index bfbd22dfea9..31b64ff3337 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function cmp_invalid_addr_as_int diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle index bfb7581b49d..9875c8c8f67 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle index 093b63521e6..0eb82222466 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function fvrange_n diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle index e789d39c37d..3d20b3ef6be 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle @@ -10,7 +10,6 @@ Function fsimple_array: { &t __retres } Function ftwo_star: { d __retres } Function fvpositive: { b } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function fsimple diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle index 3eef87eaec3..c6bec6fef07 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_f2 diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle index 6759eb2c636..6be3aa72874 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_array_in_struct_param diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle index 98a1e48694b..2801c12e3a4 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function add_1_5 diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle index e71891e1ea8..2c5447e5d1d 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle @@ -12,7 +12,6 @@ Function call_f2: { tt tmp __retres } Function f3: { p3[] k } Function call_f3: { tp tmp } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function call_f1 diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle index 884cf8a6f5c..59c0568ee15 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle index 64ce1c0a275..9a4cc941082 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function abs diff --git a/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle index 250316f99ab..0f8a43912a0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/asm.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle index e56158295b1..1296b169a5d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function check1 diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle index c80bbdfdc62..fd6a26d1a47 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function band_bool with behavior false diff --git a/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle index 62179a864c5..5199a49d5ed 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/call.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle index 887dec88157..6f58be4f1af 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle index 55a848888ce..59b50c4132f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle index c0c5ae7b8c0..514e872a600 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle index b169564f3f3..3aaad8d66c9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle index f8b89938178..6530278cbb9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle index bb09f85e02c..064a3b68491 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/cint.i:22: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function signed_bitwise diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle index 67dda1bd3fc..232d0259c30 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/combined.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle index e322ec1a1e8..a05054d57a9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/convert.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle index ec243b296db..9faa41ee552 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/copy.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function copy diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle index 4f81eda9072..0e195c8fcd2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle index 96ea7f28a84..07bf46ceb48 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle index 66b4587a6b7..da669bd36eb 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/doomed_axioms.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle index 665deb24842..97103136af1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/doomed_loop.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle index 16932140287..53bfdc8c969 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/doomed_unroll.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/doomed_unroll.i:15: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle index 6e4b15fb4d0..e71c6e9ae9a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle @@ -10,7 +10,6 @@ [wp] tests/wp_plugin/dynamic.i:87: Calls h1 [wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g [wp:calls] Dynamic call(s): 6. -[wp] Loading driver 'share/wp.driver' [wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior [wp] Warning: Missing RTE guards ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle index 61fd74dd9d8..c3ed1e741d4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle index 818a355e2d1..d987807fecd 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle index 312f0897fc5..31d6bb17966 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] tests/wp_plugin/flash-ergo.driver:2: Warning: Redefinition of logic INDEX_init [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle index 4e5d804718e..c1cd5c4035a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle index f193a1188d9..d7358dce80b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/float_driver.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 20 goals scheduled [wp:print-generated] diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle index 85e995df279..4a8215d591e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle @@ -4,7 +4,6 @@ Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function output diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle index a711e372d35..00f3e8dab4c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle @@ -6,7 +6,6 @@ Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle index 55eefc41f89..7fbd6b3ca7b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle @@ -6,7 +6,6 @@ Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle index 7e9d87ee00d..39e9f3d8359 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle @@ -4,7 +4,6 @@ Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function dequal diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle index 4249f034461..acae1296cda 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle @@ -4,7 +4,6 @@ Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function dequal diff --git a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle index 3ef9251b463..b48c65edf9e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/frame.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function alias diff --git a/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle index ca03a014002..1777e7e4198 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle index e9c5272c0cd..56fce1fae01 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: native support for coq is deprecated, use tip instead [wp] 2 goals scheduled [wp:print-generated] diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle index dcdf495be17..46f3cde2efb 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function fA diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle index 3fcaa7780cb..1b028ec86ba 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle index 25a6346f68a..4fb7c09c0aa 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle @@ -2,7 +2,6 @@ [kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing) [kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle index c816306f8df..c630d5f5437 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function validA diff --git a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle index 402be8d8ac5..296121a1db1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle index 9f80dffaa4d..1ac8bbc1f3f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle index 7b4df2e87f0..fb1d1f3185b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/invertible.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_plugin/invertible.i:17: Warning: No code nor implicit assigns clause for function main, generating default assigns from the prototype ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle index 9dd899de5f1..42f63d8aedb 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loop.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function init diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle index b477c37199d..a562cec21c9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/loopcurrent.i:12: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle index 991c9e2a2de..fad72a0a769 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/loopentry.i:12: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle index a01b081f525..ba2abdd43f8 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/loopextra.i:6: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle index 93ca42d9b44..ee4cd2e5dd9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/mask.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function compute diff --git a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle index 8faae9123de..738cdb2ffba 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle index b0884297aa8..743c3bfc6a9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_plugin/model.i:10: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 1 goal scheduled --------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle index 134cf5cfbb8..78a2178dc95 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle @@ -1,6 +1,5 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] No proof obligations diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle index 13e8d343c16..565ac6b571e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Axiomatic 'Nth' ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle index d314b7d06ef..5392e0e5e2b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f1_ok diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle index c0547370f6f..a3bcc315fda 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f1_ok diff --git a/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle index 06390f95302..b61273a928c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/params.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle index 8b4eb23ef7f..6dafe4cc77a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/plet.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Axiomatic 'Test' ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle index ec3540368c3..0697c55a730 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function diag diff --git a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle index 1ece42d9dc3..02280de6dca 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/repeat.c:47: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle index 7eb7d1df64d..979f8d1dcd4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: generate rte for memory access [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle index 3136da68bb2..14242727aae 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -no-warn-signed-overflow [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: generate rte for memory access [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for invalid bool value diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle index ec0f537db15..a19a1e491e6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -warn-unsigned-overflow [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: generate rte for memory access [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle index d5189e5215a..0e988b36311 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -wp-model 'Typed (Nat)' [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: generate rte for memory access [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle index 7a1f8d54362..e9d3ee4047a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -wp-model 'Typed (Nat)' -warn-unsigned-overflow [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: generate rte for memory access [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle index b8d50097f75..6d174fd9f0f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Nat)' [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp:rte] function job: missing rte for memory access [wp:rte] function job: missing rte for division by zero [wp:rte] function job: missing rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle index b4f10b26519..0a3228cc97c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte -wp-model 'Typed (Nat)' [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: -wp-rte can annotate memory access because -rte-mem is not set [wp:rte] function job: generate rte for division by zero [wp:rte] function job: generate rte for signed overflow diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle index c42d51cfe76..fdfb80b6c39 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_plugin/sep.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f1_none diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle index 897f3be73ba..62b9c9001fa 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function loops diff --git a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle index 9b3f58137ab..124de2a508d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] [CFG] Goal f_exits : Valid (Unreachable) [wp] [CFG] Goal g_exits : Valid (Unreachable) [wp] [CFG] Goal g_assigns : Valid (Unreachable) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle index 42a767b4657..aa233aaddc7 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/string_c.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards Goal Post-condition 'copied_contents' in 'memcpy': diff --git a/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle index bd7e4d2e01d..b0a83c5583c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/struct.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle index 29cc3bb6297..31e97c17095 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function mem diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle index d18122a712f..fde06aafdfc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle index beb2d13df62..6cad2d7458d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/trig.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle index 45858c34dea..60291308af6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function ASSIGN_NO_UNFOLD_KO diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle index ab37e2fb1b5..f681ec0f923 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function ASSIGN_NO_UNFOLD_KO diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle index 05fc31fd1c1..6dc9e4477f0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/unroll.i:20: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle index 77915655ed3..0d6d70086ee 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle index 24ef4545877..d68704a19a6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/unsafe-arrays.i:13: User Error: Invalid infinite range (shiftfield_F1_f p_0)+(..) diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle index 8f8e6a453d9..8f0c8d4ce8a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job_assigns diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle index 129e94d6af2..8f7b2282f20 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-no-volatile [...] [kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_plugin/volatile.i:15: Warning: unsafe volatile access to (term) l-value diff --git a/src/plugins/wp/tests/wp_store/oracle/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle/array.res.oracle index 70648cc14cd..cf476ad115d 100644 --- a/src/plugins/wp/tests/wp_store/oracle/array.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle/array.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_store/array.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function g diff --git a/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle index 3f1d57dc0cb..fc4518d506c 100644 --- a/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_store/natural.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle index d98e119512c..0850a3c16ed 100644 --- a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle index 5b15a883bf9..175f393e79e 100644 --- a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_store/struct.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle index e6de0501d53..1cb5b23e556 100644 --- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle +++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_tip/chunk_printing.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [rte] annotating function main ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle index 31f7225f21a..a43b8e6759f 100644 --- a/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle +++ b/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function split diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle index b461930a19a..6911b721195 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main1 diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle index a4351662142..91c35e494c2 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main1 diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle index 2aff985d9a4..fd7ab0c35a6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/avar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/avar.i:4: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle index 42142a26a79..79830d2882d 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/avar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/avar.i:4: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle index 6955c7e9f33..78f07a37773 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/bug_9.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle index d1a9c2edc88..4b6dba37d8e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/bug_9.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle index 5de789f115c..175f532ae7f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/cast_fits.i:13: Warning: Cast with incompatible pointers types (source: __anonstruct_L2_2*) diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle index 965f27bfd7d..0db2247f414 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/cast_fits.i:13: Warning: Cast with incompatible pointers types (source: __anonstruct_L2_2*) diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle index 1e91b9fe01b..ff1c02a4ba5 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/frame.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function compound diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle index 3cc68cc1bef..93b72601618 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/frame.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function compound diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle index 573cc01ba43..c00b06312b6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/mvar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/mvar.i:14: Warning: No code nor implicit assigns clause for function Write, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle index a4c11cbaf13..fef31f96530 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/mvar.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/mvar.i:14: Warning: No code nor implicit assigns clause for function Write, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle index 9fea0aa32cc..4d36bdaa42c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle index 4a80ee7c1be..4b06e83a958 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle index 1de296f9e9a..5fcad89c141 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 1 goal scheduled --------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle index dc5985c4828..d2e3f2a9cd7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle index 3716b8fceb3..115e7900443 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle index c73cb0f2080..6bddd899e5d 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle index 8db4499af68..2b7c8292fd5 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/unit_call.i:7: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle index 4d1955acf51..2fe4a448986 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [kernel] tests/wp_typed/unit_call.i:7: Warning: No code nor implicit assigns clause for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle index dfda7aa3f9a..280d1b5db6a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/unit_cast.i:4: Warning: Cast with incompatible pointers types (source: sint32*) (target: sint8*) diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle index bb48de46dd6..84e952f6019 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/unit_cast.i:4: Warning: Cast with incompatible pointers types (source: sint32*) (target: sint8*) diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle index c96410cf87b..f220848799e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle index 2dc8392a426..ac27acaa0dd 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle index bb4bf933617..157f2dd9361 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle @@ -4,7 +4,6 @@ Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle index 8dee3ca102c..8c6dba5f1eb 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle index 92ab010a2b7..dc71a1a475c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle index 7388a4baf80..508a664970f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function check diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle index 43877a40342..c0eec988340 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function check diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle index c1c14a0c647..f610bd6ab0f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function duplet diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle index e11c326de60..98b60be4d4a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function duplet diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle index 6be54b4bb09..7c21a18a61a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle index e3fed83ab4c..8d72724d212 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Global ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle index e81bad545d0..b79c6356f02 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle index ca652b49c38..f756360a105 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function bar diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle index 3ef9cfde404..5a1fdea5b33 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/unit_loopscope.i:14: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle index 62ec7355781..9cd81cf8107 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards [wp] tests/wp_typed/unit_loopscope.i:14: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle index b744d1ea2de..f3cb015dea5 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function make diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle index 8a07fab0501..c0f6bc8b083 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function make diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle index e131924404a..09bf1833614 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle index b129820adfb..33e37139a19 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle index 9d00a4ee69a..fd636bbb09f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function complex diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle index 68e873a5b9f..7af88b3ded6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function complex diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle index 056fdd1bee8..4e4f0bbf55a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function rl1 diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle index 90e88cdc057..8bb1f805315 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle @@ -1,6 +1,5 @@ # 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' [wp] Warning: Missing RTE guards [wp] No proof obligations diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle index 6d48fd74589..08ed2413253 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function caller diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle index b5584066b9c..af4d14ff9c3 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function caller diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle index e8e6e13bc58..6d82d57897c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] [CFG] Goal init_exits : Valid (Unreachable) [wp] [CFG] Goal init_t1_exits : Valid (Unreachable) [wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable) diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle index aa1fcfbc2ff..253772faadc 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] [CFG] Goal init_exits : Valid (Unreachable) [wp] [CFG] Goal init_t1_exits : Valid (Unreachable) [wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable) diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle index 01aafec9e30..b49ad5f8ddd 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function job diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle index 46d05c94af5..3df342a583b 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle index e8561738bcd..14d0ebde9e9 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Global diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle index 758429573e3..f6ac9a650ae 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_string.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function strlen diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle index d99aaaf937e..b0256f00b0c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_string.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function strlen diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle index 1bb42be2636..ed045c6b782 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle index 14d31113393..abbc64b85da 100644 --- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function main diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle index 218d938c66f..3e326765311 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_usage/caveat.i:41: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function explicit diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle index bf777e68401..b4a9f732ab5 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle @@ -11,7 +11,6 @@ Function implicit: { a *r p q } Function explicit: { a *r p q } Function observer: { a *r p q } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function explicit diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle index bb429c2780e..c4439057d74 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards [wp] tests/wp_usage/caveat2.i:22: Warning: Undefined array-size (sint32[]) ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle index 200b214f0cc..d15c7f73b49 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle @@ -1,7 +1,6 @@ # 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' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function reset diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle index a812acef1d1..253cb2dea90 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle @@ -39,7 +39,6 @@ Function calling_spec: Function cup: { val *ref &addr array[] &addr_value val_ref array_ref[] value_array } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] [CFG] Goal by_addr_in_code_annotation_requires : Valid (Unreachable) [wp] [CFG] Goal by_reference_in_code_annotation_no_exit_exits : Valid (Unreachable) [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle index d9760199b7e..fd9f352e5c8 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_usage/core.i:11: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_usage/core.i:24: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle index 68fa4441538..337bce578f7 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle @@ -3,7 +3,6 @@ [kernel] tests/wp_usage/core.i:11: Warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_usage/core.i:24: Warning: Missing assigns clause (assigns 'everything' instead) diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle index 4535eb5a131..6bb95463d0e 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Raw)' [...] [kernel] Parsing tests/wp_usage/global.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle index 504e20e6bd6..0243fc9b178 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed' [...] [kernel] Parsing tests/wp_usage/global.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle index 4e060164a41..6d03c92ee56 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_usage/global.c (with preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function foo diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle index c089fb5d1fb..2ed983d3f5f 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function memcpy_alias_vars diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle index bcd929e7df7..71a2cdaccb6 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars': diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle index b4b1200e289..4751ddf0b3f 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle @@ -1,7 +1,6 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle index 5e33a1a8de1..4b1378e9384 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle @@ -7,7 +7,6 @@ Init: { } Function f: { *ptr src idx } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] tests/wp_usage/issue-189.i:17: Warning: forbidden write to variable 'src' considered in an isolated context. diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle index 557f81f473c..0b9c5b7d7e6 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle @@ -7,7 +7,6 @@ Init: { } Function f: { *ptr src idx } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle index 45812dbfaba..1328bbed17f 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle @@ -15,6 +15,5 @@ Function declared_equals_x: { x p } Function defined_equals_x: { x p } Function recursive_usage: { x y b } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] No proof obligations diff --git a/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle index b335b1e24b1..d951b156c9d 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle @@ -1,6 +1,5 @@ [kernel] Warning: ignoring source files specified on the command line while loading a global initial context. [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' ------------------------------------------------------------ Function f ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res b/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res index 565f6392f5a..5271ccf0c21 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res +++ b/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res @@ -1,6 +1,5 @@ [kernel] Parsing tests/wp_usage/save_load.i (no preprocessing) [wp] Running WP plugin... -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards ------------------------------------------------------------ Function f diff --git a/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle index e7916ad1659..d35aef5194b 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle @@ -9,6 +9,5 @@ Function f: { &ly0 lz0 lx1 &ly1 lz1 lq0 lq1 lp1 &la0 la1 ls0 &lv0 lw0 ls1 ls2 ls3 ls4 ls5 ls6 } ................................................. -[wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] No proof obligations -- GitLab