From a9a955d1ce801ae9493391d97757517e34bfd137 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Jan 2026 12:41:37 +0000 Subject: [PATCH 1/8] Fix SMT2 output determinism by using ordered maps This commit addresses the issue where SMT2 formula output varied even when semantically equivalent C code was provided with different source formatting (e.g., adding empty lines). Root Cause: ----------- Phi nodes were generated by iterating over a hash map, implying iteration in hash-dependent order. When source code formatting changes: 1. Line numbers change 2. Expression hashes change 3. Symbols are stored/iterated in different orders 4. SMT2 declarations appear in different orders The ensuing changes to the SMT formula content -- even though the formulae were semantically equivalent -- caused variability in SMT-solver performance. Producing stable output should ensure stability in solver performance. For the test case provided in #8820 this now yields: `SMT files: 0 lines differ` (where previously it was 8 lines differing). Fixes: #8820 --- .../cbmc/deterministic-smt-output/main.c | 10 +++++++ .../cbmc/deterministic-smt-output/test.desc | 11 +++++++ regression/validate-trace-xml-schema/check.py | 1 + src/goto-symex/symex_goto.cpp | 30 +++++++++++++++++-- 4 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/deterministic-smt-output/main.c create mode 100644 regression/cbmc/deterministic-smt-output/test.desc diff --git a/regression/cbmc/deterministic-smt-output/main.c b/regression/cbmc/deterministic-smt-output/main.c new file mode 100644 index 00000000000..a621d3a95e8 --- /dev/null +++ b/regression/cbmc/deterministic-smt-output/main.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + int x; + int y; + int z = x + y; + assert(z == x + y); + return 0; +} diff --git a/regression/cbmc/deterministic-smt-output/test.desc b/regression/cbmc/deterministic-smt-output/test.desc new file mode 100644 index 00000000000..83337a751f0 --- /dev/null +++ b/regression/cbmc/deterministic-smt-output/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--smt2 --outfile - +activate-multi-line-match +\(declare-fun \|main::1::x!0@1#1\| \(\) \(_ BitVec 32\)\)(?s:.)*\(declare-fun \|main::1::y!0@1#1\| \(\) \(_ BitVec 32\)\) +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Tests that x is always declared before y, i.e., in lexicographic order. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 4dabf069c3c..c6bda7b4f4f 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -14,6 +14,7 @@ ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s[0], s[1]), [ # these tests dump the raw SMT2 output (using --outfile) ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'], + ['deterministic-smt-output', 'test.desc'], # these tests expect input from stdin ['json-interface1', 'test_wrong_option.desc'], ['json-interface1', 'test.desc'], diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 3bde290706b..b61e48f36a5 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_with_value_set.h" #include +#include void goto_symext::apply_goto_condition( goto_symex_statet ¤t_state, @@ -715,8 +716,20 @@ void goto_symext::phi_function( goto_state.get_level2().current_names.get_delta_view( dest_state.get_level2().current_names, delta_view, false); - for(const auto &delta_item : delta_view) + std::map + ordered_names_to_merge; + for(auto it = delta_view.begin(); it != delta_view.end(); ++it) { + const ssa_exprt &ssa = it->m.first; + bool inserted = + ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it}) + .second; + CHECK_RETURN(inserted); + } + + for(const auto &ordered_entry : ordered_names_to_merge) + { + const auto &delta_item = *ordered_entry.second; const ssa_exprt &ssa = delta_item.m.first; std::size_t goto_count = delta_item.m.second; std::size_t dest_count = !delta_item.is_in_both_maps() @@ -741,11 +754,22 @@ void goto_symext::phi_function( dest_state.get_level2().current_names.get_delta_view( goto_state.get_level2().current_names, delta_view, false); - for(const auto &delta_item : delta_view) + ordered_names_to_merge.clear(); + for(auto it = delta_view.begin(); it != delta_view.end(); ++it) { - if(delta_item.is_in_both_maps()) + if(it->is_in_both_maps()) continue; + const ssa_exprt &ssa = it->m.first; + bool inserted = + ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it}) + .second; + CHECK_RETURN(inserted); + } + + for(const auto &ordered_entry : ordered_names_to_merge) + { + const auto &delta_item = *ordered_entry.second; const ssa_exprt &ssa = delta_item.m.first; std::size_t goto_count = 0; std::size_t dest_count = delta_item.m.second; From 74c18a00b6235862f03234e541fe2a030ddc9ad9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:16:15 +0000 Subject: [PATCH 2/8] Set prefix for temporaries when invoking per-instruction goto conversion We otherwise set the prefix in `goto_convert_functionst::convert_function`, which is not used when directly converting individual instructions. This makes sure we have deterministic names irrespective of the order in which we iterate over functions. --- src/ansi-c/goto-conversion/goto_convert_class.h | 5 +++++ .../contracts/dynamic-frames/dfcc_instrument_loop.cpp | 7 +++++++ .../contracts/dynamic-frames/dfcc_instrument_loop.h | 4 ++++ .../contracts/dynamic-frames/dfcc_wrapper_program.cpp | 2 ++ 4 files changed, 18 insertions(+) diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 600938751f3..6ea485eeb59 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -50,6 +50,11 @@ class goto_convertt : public messaget { } + void set_prefix(const std::string &prefix) + { + tmp_symbol_prefix = prefix; + } + protected: symbol_table_baset &symbol_table; namespacet ns; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 881d16ddcb1..314890a5ca0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -138,6 +138,7 @@ void dfcc_instrument_loopt::operator()( exprt invariant(loop.invariant); const auto history_var_map = add_prehead_instructions( loop_id, + function_id, goto_function, symbol_table, head, @@ -172,6 +173,7 @@ void dfcc_instrument_loopt::operator()( add_body_instructions( loop_id, cbmc_loop_id, + function_id, goto_function, symbol_table, head, @@ -205,6 +207,7 @@ void dfcc_instrument_loopt::operator()( std::unordered_map dfcc_instrument_loopt::add_prehead_instructions( const std::size_t loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -266,6 +269,7 @@ dfcc_instrument_loopt::add_prehead_instructions( code_frontend_assignt initial_invariant_assignment{ initial_invariant, invariant, loop_head_location}; goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); converter.goto_convert( initial_invariant_assignment, pre_loop_head_instrs, language_mode); } @@ -425,6 +429,7 @@ dfcc_instrument_loopt::add_step_instructions( } goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); const irep_idt &language_mode = dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; { @@ -468,6 +473,7 @@ dfcc_instrument_loopt::add_step_instructions( void dfcc_instrument_loopt::add_body_instructions( const std::size_t loop_id, const std::size_t cbmc_loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -513,6 +519,7 @@ void dfcc_instrument_loopt::add_body_instructions( } goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); { // Because of the unconditional jump above the following code is only // reachable in the step case. Generate the inductive invariant check diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h index 8e624e016ae..0db2bb5889c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -178,6 +178,7 @@ class dfcc_instrument_loopt /// ``` /// /// \param[in] loop_id Id of the loop to transform. + /// \param[in] function_id Id of the function. /// \param[inout] goto_function The function containing the loop. /// \param[inout] symbol_table Symbol table of the model. /// \param[inout] loop_head Head node of the loop. @@ -195,6 +196,7 @@ class dfcc_instrument_loopt /// \return `history_var_map` that maps variables to loop_entry variables. std::unordered_map add_prehead_instructions( const std::size_t loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -277,6 +279,7 @@ class dfcc_instrument_loopt /// /// \param[in] loop_id Id assigned to the loop by the `cfg_info` numbering. /// \param[in] cbmc_loop_id Id assigned to the loop by CBMC's numbering. + /// \param[in] function_id Id of the function. /// \param[inout] goto_function The function containing the loop. /// \param[inout] symbol_table Symbol table of the model. /// \param[in] loop_head Head node of the loop. @@ -292,6 +295,7 @@ class dfcc_instrument_loopt void add_body_instructions( const std::size_t loop_id, const std::size_t cbmc_loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 9124f954e8d..9889951f5f4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -203,6 +203,8 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( ns(goto_model.symbol_table), converter(goto_model.symbol_table, log.get_message_handler()) { + converter.set_prefix(id2string(wrapper_symbol.name) + "::$tmp"); + // generate a return value symbol (needed to instantiate all contract lambdas) if(contract_code_type.return_type().id() != ID_empty) { From 48d263c29c589e8663f641d543418a7c1fa33862 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:21:43 +0000 Subject: [PATCH 3/8] Make goal-to-constraint conversion fully deterministic Avoid hash value changes resulting in different sequences of constraints being generated, which can affect SMT solver performance. --- src/goto-checker/goto_symex_property_decider.cpp | 2 +- src/goto-checker/goto_symex_property_decider.h | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index 51bcd5575c3..fdec0b18c19 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -63,7 +63,7 @@ void goto_symex_property_decidert:: { // it's going to be checked, but we don't know the status yet property_pair_it->second.status |= property_statust::UNKNOWN; - goal_map[property_id].instances.push_back(it); + goal_map[id2string(property_id)].instances.push_back(it); } } } diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 21b4036b65d..368416763b2 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -82,10 +82,11 @@ class goto_symex_property_decidert exprt as_expr() const; }; - /// Maintains the relation between a property ID and - /// the corresponding goal variable that encodes - /// the negation of the conjunction of the instances of the property - std::map goal_map; + /// Maintains the relation between a property ID and the corresponding goal + /// variable that encodes the negation of the conjunction of the instances of + /// the property. Uses `std::string` to maintain consistent (lexicographic) + /// ordering as we iterate over this map to produce constraints. + std::map goal_map; }; #endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H From 600f4cbd950dc583d09b3a2aa8db0939c5e3f0b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:23:05 +0000 Subject: [PATCH 4/8] Add determinism comments to SMT formula printing Explain why iteration is actually deterministic. --- src/solvers/smt2/smt2_conv.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e00becc56e9..6e1903359d3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -209,7 +209,9 @@ void smt2_convt::write_footer() { out << "\n"; - // fix up the object sizes + // Output object size definitions + // Note: object_sizes is std::map, so iteration is deterministic (sorted by + // key) for(const auto &object : object_sizes) define_object_size(object.second, object.first); @@ -243,6 +245,9 @@ void smt2_convt::write_footer() if(solver!=solvert::BOOLECTOR) { + // Output get-value commands for all identifiers + // Note: smt2_identifiers is std::set, so iteration is deterministic + // (sorted) for(const auto &id : smt2_identifiers) out << "(get-value (" << id << "))" << "\n"; @@ -5281,6 +5286,15 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr) return lowered_expr; } +/// Find and declare symbols used in an expression +/// This function traverses the expression tree and creates SMT2 declarations +/// for all symbols (variables) found. Symbols are added to identifier_map to +/// avoid duplication declarations. +/// +/// Determinism: The traversal of expression trees is deterministic, and solely +/// depends on syntactic expression structure, not expression hash codes. +/// +/// \param expr: expression to scan for symbols void smt2_convt::find_symbols(const exprt &expr) { if(is_zero_width(expr.type(), ns)) From c35d36d989b525db4f5328d2e86b23136144a3b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:24:31 +0000 Subject: [PATCH 5/8] DFCC instrumentation: deterministic initializer order Iterate over symbols in lexicographic order to ensure that we consistently produce the same instrumented program for a given input. --- .../contracts/dynamic-frames/dfcc_library.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 028893f05d9..3c4809a79b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -548,7 +548,11 @@ void dfcc_libraryt::add_instrumented_functions_map_init_instructions( auto instrumented_functions_map = get_instrumented_functions_map_symbol().symbol_expr(); - for(auto &function_id : instrumented_functions) + std::map sorted_instrumented_functions; + for(const auto &function_id : instrumented_functions) + sorted_instrumented_functions.insert({id2string(function_id), function_id}); + + for(const auto &[_, function_id] : sorted_instrumented_functions) { auto object_id = pointer_object(address_of_exprt( dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) From 97b82d67e78193dd8c4a9771bd31fef5234ffcc8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:27:58 +0000 Subject: [PATCH 6/8] Make instruction numbering fully deterministic Changes in function-identifier hashes should not result in varying location numbers. This requires updating several test descriptions that rely on specific location numbers. Also, some location numbers can vary across platforms when, e.g., system headers drag in additional functions, or 32/64-bit differences in constraining argc. To avoid such problems, several tests were adjusted to either not use unnecessary system headers or not use argc/argv. --- .../clinit-lifting2/test-goto-functions.desc | 2 +- .../clinit-lifting3/test-goto-functions.desc | 2 +- .../cprover/function_calls/call_no_body1.desc | 4 +- .../cprover/function_calls/call_no_body2.desc | 2 +- .../branching-ge/test-always-constants.desc | 4 +- .../branching-ge/test-always-intervals.desc | 4 +- .../branching-ge/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-ge/test-never-constants.desc | 4 +- .../branching-ge/test-never-intervals.desc | 4 +- .../branching-ge/test-never-value-set.desc | 4 +- .../branching-gt/test-always-constants.desc | 4 +- .../branching-gt/test-always-intervals.desc | 4 +- .../branching-gt/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-gt/test-never-constants.desc | 4 +- .../branching-gt/test-never-intervals.desc | 4 +- .../branching-gt/test-never-value-set.desc | 4 +- .../branching-le/test-always-constants.desc | 4 +- .../branching-le/test-always-intervals.desc | 4 +- .../branching-le/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-le/test-never-constants.desc | 4 +- .../branching-le/test-never-intervals.desc | 4 +- .../branching-le/test-never-value-set.desc | 4 +- .../branching-lt/test-always-constants.desc | 4 +- .../branching-lt/test-always-intervals.desc | 4 +- .../branching-lt/test-always-value-set.desc | 4 +- .../test-indeterminate-constants.desc | 4 +- .../test-indeterminate-intervals.desc | 4 +- .../test-indeterminate-value-set.desc | 4 +- .../branching-lt/test-never-constants.desc | 4 +- .../branching-lt/test-never-intervals.desc | 4 +- .../branching-lt/test-never-value-set.desc | 4 +- .../liveness-array/test-liveness.desc | 6 +- .../liveness-array/test-write-location.desc | 6 +- .../test-liveness-show.desc | 8 +-- .../test-liveness-three-way-show.desc | 8 +-- .../test-write-location-show.desc | 6 +- .../test-write-location-three-way-show.desc | 6 +- .../liveness-loop/test-liveness.desc | 8 +-- .../liveness-loop/test-write-location.desc | 8 +-- .../test-liveness.desc | 10 +-- .../test-write-location.desc | 10 +-- .../liveness-struct/test-liveness.desc | 6 +- .../liveness-struct/test-write-location.desc | 6 +- .../goto-analyzer/liveness/test-liveness.desc | 6 +- .../liveness/test-write-location.desc | 6 +- .../loop-termination-eq/test-constants.desc | 4 +- .../loop-termination-eq/test-intervals.desc | 4 +- .../loop-termination-eq/test-value-sets.desc | 4 +- .../loop-termination-ne/test-constants.desc | 4 +- .../loop-termination-ne/test-intervals.desc | 4 +- .../test-unwind-10-constants.desc | 4 +- .../test-unwind-10-intervals.desc | 4 +- .../test-unwind-10-value-sets.desc | 4 +- .../test-unwind-5-constants.desc | 4 +- .../test-unwind-5-intervals.desc | 4 +- .../test-unwind-5-value-sets.desc | 4 +- .../loop-termination-ne/test-value-sets.desc | 4 +- .../test.desc | 48 +++++++------- .../test.desc | 46 ++++++------- .../test.desc | 56 ++++++++-------- .../test.desc | 64 +++++++++---------- .../test.desc | 6 +- .../ternary-operator/test-constants.desc | 12 ++-- .../ternary-operator/test-intervals.desc | 12 ++-- .../ternary-operator/test-value-sets.desc | 2 +- .../value-set-compact-01/test.desc | 6 +- .../value-set-compact-02/test.desc | 2 +- .../value-set-compact-03/test.desc | 2 +- .../test.desc | 2 +- .../value-set-structs/test_show.desc | 2 +- .../test-constants-every-element.desc | 12 ++-- .../test-constants-smash.desc | 2 +- .../test-constants-up-to-3-elements.desc | 2 +- .../test-intervals-every-element.desc | 12 ++-- .../test-intervals-smash.desc | 2 +- .../test-intervals-up-to-3-elements.desc | 2 +- .../test-eq.desc | 6 +- .../test-gt.desc | 6 +- .../test.desc | 38 +++++------ .../test.desc | 40 ++++++------ .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../main.c | 3 - .../test.desc | 10 +-- .../test.desc | 6 +- .../test.desc | 4 +- .../test.desc | 12 ++-- .../test.desc | 10 +-- .../havoc-global-int-01/test.desc | 2 +- .../havoc-global-int-02/test.desc | 2 +- .../havoc-global-struct/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 4 +- .../without-transform.desc | 4 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../with-transform.desc | 4 +- .../without-transform.desc | 2 +- .../test.c | 2 +- .../with-transform.desc | 2 +- .../without-transform.desc | 2 +- .../goto-instrument/lexical-loops1/test.c | 8 +-- .../goto-instrument/lexical-loops1/test.desc | 2 +- .../goto-instrument/lexical-loops2/test.c | 9 +-- .../goto-instrument/lexical-loops2/test.desc | 2 +- .../goto-instrument/lexical-loops3/test.c | 9 +-- .../goto-instrument/lexical-loops3/test.desc | 2 +- .../goto-instrument/lexical-loops4/test.c | 9 +-- .../goto-instrument/lexical-loops4/test.desc | 2 +- .../goto-instrument/lexical-loops5/test.c | 9 +-- .../goto-instrument/lexical-loops5/test.desc | 4 +- .../goto-instrument/lexical-loops6/test.c | 11 ++-- .../goto-instrument/lexical-loops7/test.c | 9 +-- .../goto-instrument/lexical-loops7/test.desc | 2 +- .../goto-instrument/lexical-loops8/test.c | 12 ++-- .../goto-instrument/lexical-loops8/test.desc | 2 +- .../goto-instrument/lexical-loops9/test.c | 11 ++-- .../goto-instrument/lexical-loops9/test.desc | 2 +- .../natural-loops-multiple-backedges/main.c | 12 ++-- .../test.desc | 6 +- src/goto-programs/goto_functions.cpp | 5 +- 153 files changed, 473 insertions(+), 466 deletions(-) diff --git a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc index f9d8e26f17a..5359377052e 100644 --- a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc +++ b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc @@ -4,7 +4,7 @@ Test activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\s*// 0 no location\n\s*CALL java::Other\.\(\)\s*// 1 no location\s*DECL .*::total +\s*// 26 no location\n\s*CALL java::Other\.\(\)\s*// 27 no location\s*DECL .*::total -- -- This checks that the clinit-wrapper function is called once, even though there are two calls in the source diff --git a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc index f3c4410882b..8af9ab4bf47 100644 --- a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc +++ b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc @@ -4,7 +4,7 @@ Test activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\s*// 0 no location\n\s*CALL java::Other\.\(\)\s*// 1 no location\s*CALL java::Third\.\(\)\s*// 2 no location\s*DECL .*::total +\s*// 28 no location\n\s*CALL java::Other\.\(\)\s*// 29 no location\s*CALL java::Third\.\(\)\s*// 30 no location\s*DECL .*::total -- -- This checks that the clinit-wrapper function is called once, even though there are two calls in the source diff --git a/regression/cprover/function_calls/call_no_body1.desc b/regression/cprover/function_calls/call_no_body1.desc index dc99c1876ad..a2b2967037a 100644 --- a/regression/cprover/function_calls/call_no_body1.desc +++ b/regression/cprover/function_calls/call_no_body1.desc @@ -4,6 +4,6 @@ call_no_body1.c ^EXIT=0$ ^SIGNAL=0$ ^\*\*\*\* WARNING: no body for function function_without_body$ -^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S18\.2-0\]\)$ -^\(\d+\) ∀ ς : state \. S18\.2\(ς\) ⇒ S18\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ +^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S2\.14-0\]\)$ +^\(\d+\) ∀ ς : state \. S2\.14\(ς\) ⇒ S2\.15\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ -- diff --git a/regression/cprover/function_calls/call_no_body2.desc b/regression/cprover/function_calls/call_no_body2.desc index 9615edec2f8..45571cb3249 100644 --- a/regression/cprover/function_calls/call_no_body2.desc +++ b/regression/cprover/function_calls/call_no_body2.desc @@ -3,5 +3,5 @@ call_no_body2.c --text ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S18\.2-0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S2\.14-0\]\)$ -- diff --git a/regression/goto-analyzer/branching-ge/test-always-constants.desc b/regression/goto-analyzer/branching-ge/test-always-constants.desc index 73167c183a9..1cf5f793ec0 100644 --- a/regression/goto-analyzer/branching-ge/test-always-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-always-intervals.desc b/regression/goto-analyzer/branching-ge/test-always-intervals.desc index e35fdffedda..43357551fa6 100644 --- a/regression/goto-analyzer/branching-ge/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-always-value-set.desc b/regression/goto-analyzer/branching-ge/test-always-value-set.desc index 6fa9bae0c29..6117f6ae26f 100644 --- a/regression/goto-analyzer/branching-ge/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc index 406cd930231..a73dee0319b 100644 --- a/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-constants.desc b/regression/goto-analyzer/branching-ge/test-never-constants.desc index 2d1d6df13a0..6636668ae53 100644 --- a/regression/goto-analyzer/branching-ge/test-never-constants.desc +++ b/regression/goto-analyzer/branching-ge/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-intervals.desc b/regression/goto-analyzer/branching-ge/test-never-intervals.desc index 9c31600de4f..0547e50930f 100644 --- a/regression/goto-analyzer/branching-ge/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-ge/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-value-set.desc b/regression/goto-analyzer/branching-ge/test-never-value-set.desc index f8f2a0aa278..b6ad4fe65f7 100644 --- a/regression/goto-analyzer/branching-ge/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-ge/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-constants.desc b/regression/goto-analyzer/branching-gt/test-always-constants.desc index 73167c183a9..1cf5f793ec0 100644 --- a/regression/goto-analyzer/branching-gt/test-always-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-intervals.desc b/regression/goto-analyzer/branching-gt/test-always-intervals.desc index e35fdffedda..43357551fa6 100644 --- a/regression/goto-analyzer/branching-gt/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-value-set.desc b/regression/goto-analyzer/branching-gt/test-always-value-set.desc index 6fa9bae0c29..6117f6ae26f 100644 --- a/regression/goto-analyzer/branching-gt/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc index 406cd930231..a73dee0319b 100644 --- a/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-constants.desc b/regression/goto-analyzer/branching-gt/test-never-constants.desc index 2d1d6df13a0..6636668ae53 100644 --- a/regression/goto-analyzer/branching-gt/test-never-constants.desc +++ b/regression/goto-analyzer/branching-gt/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-intervals.desc b/regression/goto-analyzer/branching-gt/test-never-intervals.desc index 9c31600de4f..0547e50930f 100644 --- a/regression/goto-analyzer/branching-gt/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-gt/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-value-set.desc b/regression/goto-analyzer/branching-gt/test-never-value-set.desc index f8f2a0aa278..b6ad4fe65f7 100644 --- a/regression/goto-analyzer/branching-gt/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-gt/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-constants.desc b/regression/goto-analyzer/branching-le/test-always-constants.desc index 73167c183a9..1cf5f793ec0 100644 --- a/regression/goto-analyzer/branching-le/test-always-constants.desc +++ b/regression/goto-analyzer/branching-le/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-intervals.desc b/regression/goto-analyzer/branching-le/test-always-intervals.desc index e35fdffedda..43357551fa6 100644 --- a/regression/goto-analyzer/branching-le/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-value-set.desc b/regression/goto-analyzer/branching-le/test-always-value-set.desc index 6fa9bae0c29..6117f6ae26f 100644 --- a/regression/goto-analyzer/branching-le/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc index 406cd930231..a73dee0319b 100644 --- a/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-constants.desc b/regression/goto-analyzer/branching-le/test-never-constants.desc index 2d1d6df13a0..6636668ae53 100644 --- a/regression/goto-analyzer/branching-le/test-never-constants.desc +++ b/regression/goto-analyzer/branching-le/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-intervals.desc b/regression/goto-analyzer/branching-le/test-never-intervals.desc index 9c31600de4f..0547e50930f 100644 --- a/regression/goto-analyzer/branching-le/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-le/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-value-set.desc b/regression/goto-analyzer/branching-le/test-never-value-set.desc index f8f2a0aa278..b6ad4fe65f7 100644 --- a/regression/goto-analyzer/branching-le/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-le/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-constants.desc b/regression/goto-analyzer/branching-lt/test-always-constants.desc index 73167c183a9..1cf5f793ec0 100644 --- a/regression/goto-analyzer/branching-lt/test-always-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-always-constants.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-intervals.desc b/regression/goto-analyzer/branching-lt/test-always-intervals.desc index e35fdffedda..43357551fa6 100644 --- a/regression/goto-analyzer/branching-lt/test-always-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-always-intervals.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[5, 5\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-value-set.desc b/regression/goto-analyzer/branching-lt/test-always-value-set.desc index 6fa9bae0c29..6117f6ae26f 100644 --- a/regression/goto-analyzer/branching-lt/test-always-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-always-value-set.desc @@ -3,6 +3,6 @@ main-always.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc index 406cd930231..a73dee0319b 100644 --- a/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc @@ -3,6 +3,6 @@ main-indeterminate.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-constants.desc b/regression/goto-analyzer/branching-lt/test-never-constants.desc index 2d1d6df13a0..6636668ae53 100644 --- a/regression/goto-analyzer/branching-lt/test-never-constants.desc +++ b/regression/goto-analyzer/branching-lt/test-never-constants.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* TOP @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-intervals.desc b/regression/goto-analyzer/branching-lt/test-never-intervals.desc index 9c31600de4f..0547e50930f 100644 --- a/regression/goto-analyzer/branching-lt/test-never-intervals.desc +++ b/regression/goto-analyzer/branching-lt/test-never-intervals.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-value-set.desc b/regression/goto-analyzer/branching-lt/test-never-value-set.desc index f8f2a0aa278..b6ad4fe65f7 100644 --- a/regression/goto-analyzer/branching-lt/test-never-value-set.desc +++ b/regression/goto-analyzer/branching-lt/test-never-value-set.desc @@ -3,6 +3,6 @@ main-never.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/liveness-array/test-liveness.desc b/regression/goto-analyzer/liveness-array/test-liveness.desc index 8c5d381893a..c356511fad2 100644 --- a/regression/goto-analyzer/liveness-array/test-liveness.desc +++ b/regression/goto-analyzer/liveness-array/test-liveness.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\] -^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* \{\[0\] = \[0, 0\] @ \[16\] +^main::1::x .* \{\[0\] = \[2, 3\] @ \[21\] -- diff --git a/regression/goto-analyzer/liveness-array/test-write-location.desc b/regression/goto-analyzer/liveness-array/test-write-location.desc index 03a3569f0a5..eb67687fca6 100644 --- a/regression/goto-analyzer/liveness-array/test-write-location.desc +++ b/regression/goto-analyzer/liveness-array/test-write-location.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\] -^main::1::x .* \{\[0\] = \[2, 3\] @ \[4, 6\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* \{\[0\] = \[0, 0\] @ \[16\] +^main::1::x .* \{\[0\] = \[2, 3\] @ \[18, 20\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc index c1501370247..3543c73dac6 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] -globalX .* TOP @ \[18\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] +globalX .* TOP @ \[16\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc index 2c13d44ae4b..dfb3fa6c91a 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] -globalX .* TOP @ \[18\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] +globalX .* TOP @ \[16\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc index f3fd23e0665..2cb7e0cad8e 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* TOP @ \[0, 3\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* TOP @ \[17, 20\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc index 242a87dda34..ec74cea9f1a 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] -- diff --git a/regression/goto-analyzer/liveness-loop/test-liveness.desc b/regression/goto-analyzer/liveness-loop/test-liveness.desc index b50010b61f9..53df8cce673 100644 --- a/regression/goto-analyzer/liveness-loop/test-liveness.desc +++ b/regression/goto-analyzer/liveness-loop/test-liveness.desc @@ -3,8 +3,8 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[9\] -^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[5\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[23\] +^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/liveness-loop/test-write-location.desc b/regression/goto-analyzer/liveness-loop/test-write-location.desc index cab664fd94b..d8a36a9bc7a 100644 --- a/regression/goto-analyzer/liveness-loop/test-write-location.desc +++ b/regression/goto-analyzer/liveness-loop/test-write-location.desc @@ -3,8 +3,8 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[8\] -^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[2, 8\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[22\] +^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[16, 22\] -- diff --git a/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc b/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc index ec4dcc87fb0..9c3b45e8d05 100644 --- a/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc +++ b/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[9\] -^main::1::p .* TOP @ \[3\] -^main::1::p .*\(main::1::x\) @ \[4\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[23\] +^main::1::p .* TOP @ \[17\] +^main::1::p .*\(main::1::x\) @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc b/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc index 31c65e49a13..51bfdd976c3 100644 --- a/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc +++ b/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[6, 8\] -^main::1::p .* TOP @ \[3\] -^main::1::p .*\(main::1::x\) @ \[4\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[20, 22\] +^main::1::p .* TOP @ \[17\] +^main::1::p .*\(main::1::x\) @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-struct/test-liveness.desc b/regression/goto-analyzer/liveness-struct/test-liveness.desc index 79deb6fb562..0088b407a97 100644 --- a/regression/goto-analyzer/liveness-struct/test-liveness.desc +++ b/regression/goto-analyzer/liveness-struct/test-liveness.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::s .* \{\} @ \[1\] -^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\] -^main::1::s .* \{.x=\[2, 3\] @ \[7\], .y=\[3, 3\] @ \[2\]\} @ \[7\] +^main::1::s .* \{\} @ \[15\] +^main::1::s .* \{.x=\[1, 1\] @ \[16\], .y=\[3, 3\] @ \[16\]\} @ \[16\] +^main::1::s .* \{.x=\[2, 3\] @ \[21\], .y=\[3, 3\] @ \[16\]\} @ \[21\] -- diff --git a/regression/goto-analyzer/liveness-struct/test-write-location.desc b/regression/goto-analyzer/liveness-struct/test-write-location.desc index 4341cf79a66..e624ee1fd59 100644 --- a/regression/goto-analyzer/liveness-struct/test-write-location.desc +++ b/regression/goto-analyzer/liveness-struct/test-write-location.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-structs every-field --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::s .* \{\} @ \[1\] -^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\] -^main::1::s .* \{.x=\[2, 3\] @ \[4, 6\], .y=\[3, 3\] @ \[2\]\} @ \[4, 6\] +^main::1::s .* \{\} @ \[15\] +^main::1::s .* \{.x=\[1, 1\] @ \[16\], .y=\[3, 3\] @ \[16\]\} @ \[16\] +^main::1::s .* \{.x=\[2, 3\] @ \[18, 20\], .y=\[3, 3\] @ \[16\]\} @ \[18, 20\] -- diff --git a/regression/goto-analyzer/liveness/test-liveness.desc b/regression/goto-analyzer/liveness/test-liveness.desc index 116a242f851..453acaaf0d2 100644 --- a/regression/goto-analyzer/liveness/test-liveness.desc +++ b/regression/goto-analyzer/liveness/test-liveness.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[21\] -- diff --git a/regression/goto-analyzer/liveness/test-write-location.desc b/regression/goto-analyzer/liveness/test-write-location.desc index 9c4c2614cf6..da12efeab53 100644 --- a/regression/goto-analyzer/liveness/test-write-location.desc +++ b/regression/goto-analyzer/liveness/test-write-location.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[4, 6\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[18, 20\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-constants.desc b/regression/goto-analyzer/loop-termination-eq/test-constants.desc index cd1436ce709..65f75a7ea6d 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-constants.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-intervals.desc b/regression/goto-analyzer/loop-termination-eq/test-intervals.desc index a9b65006620..dec8c221280 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-intervals.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[0, 5\] @ \[3, 6\] -^main::1::p .* \[1, 20\] @ \[1, 5\] +^main::1::1::i .* \[0, 5\] @ \[17, 20\] +^main::1::p .* \[1, 20\] @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc b/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc index 3a55e2428c3..61883081e16 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[3, 6\] -^main::1::p .* @ \[1, 5\] +^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[17, 20\] +^main::1::p .* @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-constants.desc index cd1436ce709..65f75a7ea6d 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-intervals.desc index a9b65006620..dec8c221280 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[0, 5\] @ \[3, 6\] -^main::1::p .* \[1, 20\] @ \[1, 5\] +^main::1::1::i .* \[0, 5\] @ \[17, 20\] +^main::1::p .* \[1, 20\] @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc index b9cebc9217d..01fc39c1a50 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* 5 @ \[6\] -^main::1::p .* 32 @ \[5\] +^main::1::1::i .* 5 @ \[20\] +^main::1::p .* 32 @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc index d8ad7291409..168380bf40a 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[5, 5\] @ \[6\] -^main::1::p .* \[20, 20\] @ \[5\] +^main::1::1::i .* \[5, 5\] @ \[20\] +^main::1::p .* \[20, 20\] @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc index c5f08aa4a9f..d323bda32ff 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\] -^main::1::p .* value-set-begin: 32 :value-set-end @ \[5\] +^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[20\] +^main::1::p .* value-set-begin: 32 :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc index 139bc112faf..f44f0c5f14f 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc index 764b37add8b..819a482ca92 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[5, 5\] @ \[6\] -^main::1::p .* \[2, 1F9\] @ \[5\] +^main::1::1::i .* \[5, 5\] @ \[20\] +^main::1::p .* \[2, 1F9\] @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc index e21b91feec0..ebbbb404bfd 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\] -^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\] +^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[20\] +^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc index 3a55e2428c3..61883081e16 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[3, 6\] -^main::1::p .* @ \[1, 5\] +^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[17, 20\] +^main::1::p .* @ \[15, 19\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc index 76ce8dc8e74..add83bfdbde 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -5,27 +5,27 @@ sensitivity_dependency_arrays.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_arrays::1::bool_ \(\) -> TOP @ \[10\] -do_arrays::1::bool_1 \(\) -> TOP @ \[11\] -do_arrays::1::bool_2 \(\) -> TOP @ \[12\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\] -do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\] -do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\] -do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\] +main#return_value \(\) -> TOP @ \[49\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_arrays::1::bool_ \(\) -> TOP @ \[14\] +do_arrays::1::bool_1 \(\) -> TOP @ \[15\] +do_arrays::1::bool_2 \(\) -> TOP @ \[16\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[18\]\n\} @ \[18\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[18\]\n\[1\] = 20 @ \[19\]\n\} @ \[19\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 20 @ \[19\]\n\} @ \[20\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 40 @ \[21\]\n\} @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 30 @ \[22\]\n\} @ \[22\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[23\]\n\[1\] = 30 @ \[22\]\n\} @ \[23\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[24\]\n\[1\] = 30 @ \[22\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[25\]\n\[1\] = 30 @ \[22\]\n\} @ \[25\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[25\]\n\[1\] = 10 @ \[26\]\n\} @ \[26\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[28\]\n\[1\] = 10 @ \[26\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[28\, 30\]\n\[1\] = 10 @ \[26\]\n\} @ \[28\, 30\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[32]\n\[1\] = 10 @ \[26\]\n\} @ \[32\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[34]\n\[1\] = 10 @ \[26\]\n\} @ \[34\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[34\, 36]\n\[1\] = 10 @ \[26\]\n\} @ \[34\, 36\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[34\, 36\, 39]\n\[1\] = 10 @ \[41\]\n\} @ \[41\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[42]\n\[1\] = 10 @ \[41\]\n\} @ \[42\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc index a721884d5bc..76dee873c3a 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -5,26 +5,26 @@ sensitivity_dependency_pointers.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_pointers::1::bool_ \(\) -> TOP @ \[10\] -do_pointers::1::bool_1 \(\) -> TOP @ \[11\] -do_pointers::1::bool_2 \(\) -> TOP @ \[12\] -do_pointers::1::x \(\) -> TOP @ \[13\] -do_pointers::1::x \(\) -> 10 @ \[14\] -do_pointers::1::x_p \(\) -> TOP @ \[15\] -do_pointers::1::y \(\) -> TOP @ \[16\] -do_pointers::1::y \(\) -> 20 @ \[17\] -do_pointers::1::y_p \(\) -> TOP @ \[18\] -do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\] -do_pointers::1::x \(\) -> 30 @ \[20\] -do_pointers::1::x \(\) -> 40 @ \[21\] -do_pointers::1::x \(\) -> TOP @ \[22\] -do_pointers::1::x \(\) -> 50 @ \[23\] -do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\] -do_pointers::1::x \(\) -> 60 @ \[25\] -do_pointers::1::j \(\) -> TOP @ \[26\] -do_pointers::1::j \(\) -> 60 @ \[27\] +main#return_value \(\) -> TOP @ \[42\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_pointers::1::bool_ \(\) -> TOP @ \[14\] +do_pointers::1::bool_1 \(\) -> TOP @ \[15\] +do_pointers::1::bool_2 \(\) -> TOP @ \[16\] +do_pointers::1::x \(\) -> TOP @ \[17\] +do_pointers::1::x \(\) -> 10 @ \[18\] +do_pointers::1::x_p \(\) -> TOP @ \[19\] +do_pointers::1::y \(\) -> TOP @ \[20\] +do_pointers::1::y \(\) -> 20 @ \[21\] +do_pointers::1::y_p \(\) -> TOP @ \[22\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[23\] +do_pointers::1::x \(\) -> 30 @ \[24\] +do_pointers::1::x \(\) -> 40 @ \[25\] +do_pointers::1::x \(\) -> TOP @ \[26\] +do_pointers::1::x \(\) -> 50 @ \[27\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\] +do_pointers::1::x \(\) -> 60 @ \[29\] +do_pointers::1::j \(\) -> TOP @ \[30\] +do_pointers::1::j \(\) -> 60 @ \[31\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc index 6dbe225f070..2f466a90036 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -5,32 +5,32 @@ sensitivity_dependency_structs.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_structs::1::bool_ \(\) -> TOP @ \[10\] -do_structs::1::bool_1 \(\) -> TOP @ \[11\] -do_structs::1::bool_2 \(\) -> TOP @ \[12\] -do_structs::1::st \(\) -> \{\} @ \[13\] -do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\] -do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\] -do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\] -do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\] -do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\] -do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\] -do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\] -do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\] -do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\] -do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\] -do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\] -do_structs::1::new_age \(\) -> \{\} @ \[39\] -do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\] +main#return_value \(\) -> TOP @ \[52\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_structs::1::bool_ \(\) -> TOP @ \[14\] +do_structs::1::bool_1 \(\) -> TOP @ \[15\] +do_structs::1::bool_2 \(\) -> TOP @ \[16\] +do_structs::1::st \(\) -> \{\} @ \[17\] +do_structs::1::st \(\) -> \{.x=10 @ \[18\]\} @ \[18\] +do_structs::1::st \(\) -> \{.x=10 @ \[18\]\, .y=20 @ \[19\]\} @ \[19\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=20 @ \[19\]\} @ \[20\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=40 @ \[21\]\} @ \[21\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=30 @ \[22\]\} @ \[22\] +do_structs::1::st \(\) -> \{.x=30 @ \[23\]\, .y=30 @ \[22\]\} @ \[23\] +do_structs::1::st \(\) -> \{.x=5 @ \[24\]\, .y=30 @ \[22\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=15 @ \[25\]\, .y=30 @ \[22\]\} @ \[25\] +do_structs::1::st \(\) -> \{.x=15 @ \[25\]\, .y=10 @ \[26\]\} @ \[26\] +do_structs::1::st \(\) -> \{.x=20 @ \[28\]\, .y=10 @ \[26\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=20 @ \[28\, 30\]\, .y=10 @ \[26\]\} @ \[28\, 30\] +do_structs::1::st \(\) -> \{.x=0 @ \[32\]\, .y=10 @ \[26\]\} @ \[32\] +do_structs::1::st \(\) -> \{.x=3 @ \[34\]\, .y=10 @ \[26\]\} @ \[34\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\]\, .y=10 @ \[26\]\} @ \[34\, 36\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\, 39\]\, .y=10 @ \[26\]\} @ \[34\, 36\, 39\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\, 39\]\, .y=10 @ \[41\]\} @ \[41\] +do_structs::1::st \(\) -> \{.x=20 @ \[42\]\, .y=10 @ \[41\]\} @ \[42\] +do_structs::1::new_age \(\) -> \{\} @ \[43\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[44\]\, .y=10 @ \[44\]\} @ \[44\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc index 4247d96b87e..52b0ea6107a 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -3,36 +3,36 @@ sensitivity_dependency_variables.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -global_x \(\) -> 0 @ \[9\] -do_variables::1::bool_ \(\) -> TOP @ \[11\] -do_variables::1::bool_1 \(\) -> TOP @ \[12\] -do_variables::1::bool_2 \(\) -> TOP @ \[13\] -global_x \(\) -> 5 @ \[14\] -do_variables::1::x \(\) -> TOP @ \[15\] -do_variables::1::x \(\) -> 10 @ \[16\] -do_variables::1::y \(\) -> TOP @ \[17\] -do_variables::1::y \(\) -> 20 @ \[18\] -do_variables::1::x \(\) -> 30 @ \[19\] -do_variables::1::y \(\) -> 40 @ \[20\] -do_variables::1::y \(\) -> 30 @ \[21\] -do_variables::1::x \(\) -> 30 @ \[22\] -do_variables::1::x \(\) -> 5 @ \[23\] -do_variables::1::x \(\) -> 15 @ \[24\] -do_variables::1::y \(\) -> 10 @ \[25\] -do_variables::1::x \(\) -> 20 @ \[27\] -do_variables::1::x \(\) -> 20 @ \[27\, 29\] -do_variables::1::x \(\) -> 50 @ \[31\] -do_variables::1::x \(\) -> 20 @ \[33\] -do_variables::1::x \(\) -> TOP @ \[33\, 35\] -do_variables::1::x \(\) -> 0 @ \[37\] -do_variables::1::x \(\) -> 3 @ \[39\] -do_variables::1::x \(\) -> TOP @ \[39\, 41\] -do_variables::1::x \(\) -> TOP @ \[39\, 41\, 44\] -do_variables::1::y \(\) -> 10 @ \[46\] -do_variables::1::x \(\) -> 20 @ \[47\] +main#return_value \(\) -> TOP @ \[59\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +global_x \(\) -> 0 @ \[13\] +do_variables::1::bool_ \(\) -> TOP @ \[15\] +do_variables::1::bool_1 \(\) -> TOP @ \[16\] +do_variables::1::bool_2 \(\) -> TOP @ \[17\] +global_x \(\) -> 5 @ \[18\] +do_variables::1::x \(\) -> TOP @ \[19\] +do_variables::1::x \(\) -> 10 @ \[20\] +do_variables::1::y \(\) -> TOP @ \[21\] +do_variables::1::y \(\) -> 20 @ \[22\] +do_variables::1::x \(\) -> 30 @ \[23\] +do_variables::1::y \(\) -> 40 @ \[24\] +do_variables::1::y \(\) -> 30 @ \[25\] +do_variables::1::x \(\) -> 30 @ \[26\] +do_variables::1::x \(\) -> 5 @ \[27\] +do_variables::1::x \(\) -> 15 @ \[28\] +do_variables::1::y \(\) -> 10 @ \[29\] +do_variables::1::x \(\) -> 20 @ \[31\] +do_variables::1::x \(\) -> 20 @ \[31\, 33\] +do_variables::1::x \(\) -> 50 @ \[35\] +do_variables::1::x \(\) -> 20 @ \[37\] +do_variables::1::x \(\) -> TOP @ \[37\, 39\] +do_variables::1::x \(\) -> 0 @ \[41\] +do_variables::1::x \(\) -> 3 @ \[43\] +do_variables::1::x \(\) -> TOP @ \[43\, 45\] +do_variables::1::x \(\) -> TOP @ \[43\, 45\, 48\] +do_variables::1::y \(\) -> 10 @ \[50\] +do_variables::1::x \(\) -> 20 @ \[51\] -- diff --git a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc index dbb5f0664f5..1b0cf764239 100644 --- a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc +++ b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc @@ -5,8 +5,8 @@ data-dependency-context.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -st \(\) -> \{.a=.* @ \[2, 42\]\[Data dependencies: 42, 2\]\[Data dominators: \], .b=.* @ \[5, 42\]\[Data dependencies: 42, 5\]\[Data dominators: \]\} @ \[2, 5, 42\]\[Data dependencies: 42, 5, 2\]\[Data dominators: 42\] -ar \(\) -> \{\[0\] = TOP @ \[11\, 36\]\[Data dependencies: 36\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 36\]\[Data dependencies: 36\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 36\]\[Data dependencies: 36\, 14\, 11\]\[Data dominators: 36\] -arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 37\] +st \(\) -> \{.a=.* @ \[16, 20\]\[Data dependencies: 20, 16\]\[Data dominators: \], .b=.* @ \[16, 23\]\[Data dependencies: 23, 16\]\[Data dominators: \]\} @ \[16, 20, 23\]\[Data dependencies: 23, 20, 16\]\[Data dominators: 16\] +ar \(\) -> \{\[0\] = TOP @ \[10, 29\]\[Data dependencies: 29, 10\]\[Data dominators: \]\n\[1\] = TOP @ \[10, 32\]\[Data dependencies: 32, 10\]\[Data dominators: \]\n\} @ \[10, 29, 32]\[Data dependencies: 32, 29, 10]\[Data dominators: 10\] +arr \(\) -> \{\[0\] = 1 @ \[37\]\[Data dependencies: 37\]\[Data dominators: 37\]\n\[1\] = 2 @ \[38\]\[Data dependencies: 38\]\[Data dominators: 38\]\n\[2\] = TOP @ \[39, 41\]\[Data dependencies: 41, 39\]\[Data dominators: \]\n\} @ \[39, 41\]\[Data dependencies: 41, 39\]\[Data dominators: 11\] -- ^warning: ignoring diff --git a/regression/goto-analyzer/ternary-operator/test-constants.desc b/regression/goto-analyzer/ternary-operator/test-constants.desc index e1066c6b418..9b82ccbfe11 100644 --- a/regression/goto-analyzer/ternary-operator/test-constants.desc +++ b/regression/goto-analyzer/ternary-operator/test-constants.desc @@ -3,10 +3,10 @@ main.c --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> TRUE @ \[2\] -main::1::b2 \(\) -> FALSE @ \[3\] -main::1::b3 \(\) -> TOP @ \[5\] -main::1::i \(\) -> 10 @ \[7\] -main::1::j \(\) -> 20 @ \[9\] -main::1::k \(\) -> TOP @ \[11\] +main::1::b1 \(\) -> TRUE @ \[17\] +main::1::b2 \(\) -> FALSE @ \[18\] +main::1::b3 \(\) -> TOP @ \[20\] +main::1::i \(\) -> 10 @ \[22\] +main::1::j \(\) -> 20 @ \[24\] +main::1::k \(\) -> TOP @ \[26\] -- diff --git a/regression/goto-analyzer/ternary-operator/test-intervals.desc b/regression/goto-analyzer/ternary-operator/test-intervals.desc index 03e52dd051d..e5fe50abe6d 100644 --- a/regression/goto-analyzer/ternary-operator/test-intervals.desc +++ b/regression/goto-analyzer/ternary-operator/test-intervals.desc @@ -3,10 +3,10 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> \[1, 1\] @ \[2\] -main::1::b2 \(\) -> \[0, 0\] @ \[3\] -main::1::b3 \(\) -> TOP @ \[5\] -main::1::i \(\) -> \[A, A\] @ \[7\] -main::1::j \(\) -> \[14, 14\] @ \[9\] -main::1::k \(\) -> \[A, 14\] @ \[11\] +main::1::b1 \(\) -> \[1, 1\] @ \[17\] +main::1::b2 \(\) -> \[0, 0\] @ \[18\] +main::1::b3 \(\) -> TOP @ \[20\] +main::1::i \(\) -> \[A, A\] @ \[22\] +main::1::j \(\) -> \[14, 14\] @ \[24\] +main::1::k \(\) -> \[A, 14\] @ \[26\] -- diff --git a/regression/goto-analyzer/ternary-operator/test-value-sets.desc b/regression/goto-analyzer/ternary-operator/test-value-sets.desc index be593b76d7e..2befe2d6e77 100644 --- a/regression/goto-analyzer/ternary-operator/test-value-sets.desc +++ b/regression/goto-analyzer/ternary-operator/test-value-sets.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end -main::1::b3 \(\) -> TOP @ \[5\] +main::1::b3 \(\) -> TOP @ \[20\] main::1::i \(\) -> value-set-begin: 10 :value-set-end main::1::j \(\) -> value-set-begin: 20 :value-set-end main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end diff --git a/regression/goto-analyzer/value-set-compact-01/test.desc b/regression/goto-analyzer/value-set-compact-01/test.desc index b1b03936035..76629deaacf 100644 --- a/regression/goto-analyzer/value-set-compact-01/test.desc +++ b/regression/goto-analyzer/value-set-compact-01/test.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] -main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\] -main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\] +main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[16, 27, 30, 33, 36, 39, 41\] +main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[18, 28, 31, 34, 37\] +main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[45\] -- diff --git a/regression/goto-analyzer/value-set-compact-02/test.desc b/regression/goto-analyzer/value-set-compact-02/test.desc index c5100073360..e0c0827a1f7 100644 --- a/regression/goto-analyzer/value-set-compact-02/test.desc +++ b/regression/goto-analyzer/value-set-compact-02/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\] +main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[16, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53\] -- diff --git a/regression/goto-analyzer/value-set-compact-03/test.desc b/regression/goto-analyzer/value-set-compact-03/test.desc index 64f922f90a4..b25b0d32b00 100644 --- a/regression/goto-analyzer/value-set-compact-03/test.desc +++ b/regression/goto-analyzer/value-set-compact-03/test.desc @@ -3,5 +3,5 @@ main.c --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .* +main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[16, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53\]\} .* -- diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index 67de292e3c8..139377efe1a 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc @@ -5,7 +5,7 @@ main.c ^file main.c line 46 function main: replacing function pointer by 2 possible targets$ ^file main.c line 54 function main: replacing function pointer by 2 possible targets$ ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end -^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[29, 31\]} @ \[29, 31\] +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[49, 51\]} @ \[49, 51\] ^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/value-set-structs/test_show.desc b/regression/goto-analyzer/value-set-structs/test_show.desc index 6af0a82da4b..4fa75995671 100644 --- a/regression/goto-analyzer/value-set-structs/test_show.desc +++ b/regression/goto-analyzer/value-set-structs/test_show.desc @@ -2,7 +2,7 @@ CORE main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check activate-multi-line-match -main::1::s_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0 :value-set-end @ \[16\], \.str=\{\[0\] = value-set-begin: 'x', 'y' :value-set-end @ \[16\]\n\[1\] = value-set-begin: '\\n' :value-set-end +main::1::s_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0 :value-set-end @ \[30\], \.str=\{\[0\] = value-set-begin: 'x', 'y' :value-set-end @ \[30\]\n\[1\] = value-set-begin: '\\n' :value-set-end main::1::u_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0, 3\.0 :value-set-end @ \[..\], \.str=\{\[0\] = value-set-begin: 'x', 'y', 'z' :value-set-end @ \[..\]\n\[1\] = value-set-begin: '\\n' :value-set-end @ \[..\]\n} @ \[..\]} @ \[..\] ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc index b2af6dc12d1..282c0eb459d 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays every-element ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] -main::1::arr_0_after_write \(\) -> TOP @ \[18\] -main::1::arr_1_after_write \(\) -> TOP @ \[20\] -main::1::arr_2_after_write \(\) -> TOP @ \[22\] -main::1::arr_3_after_write \(\) -> TOP @ \[24\] -main::1::arr_4_after_write \(\) -> TOP @ \[26\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] +main::1::arr_0_after_write \(\) -> TOP @ \[32\] +main::1::arr_1_after_write \(\) -> TOP @ \[34\] +main::1::arr_2_after_write \(\) -> TOP @ \[36\] +main::1::arr_3_after_write \(\) -> TOP @ \[38\] +main::1::arr_4_after_write \(\) -> TOP @ \[40\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc index e3dad3c4c5b..055d7108600 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays smash ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] main::1::arr_0_after_write \(\) -> TOP main::1::arr_1_after_write \(\) -> TOP main::1::arr_2_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc index 13608b5a3bb..0fb28b7339e 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] main::1::arr_0_after_write \(\) -> TOP main::1::arr_1_after_write \(\) -> TOP main::1::arr_2_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc index 546c92749d6..0d2e9979e50 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\] -main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\] -main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\] -main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\] -main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\] -main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\] +main::1::arr_at_ix \(\) -> \[1, 3\] @ \[23\] +main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[32\] +main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[34\] +main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[36\] +main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[38\] +main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[40\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc index 229799ca354..5c04a453736 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays smash ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[23\] main::1::arr_0_after_write \(\) -> \[1, 63\] main::1::arr_1_after_write \(\) -> \[1, 63\] main::1::arr_2_after_write \(\) -> \[1, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc index 3076e43a8eb..77a130481b7 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[23\] main::1::arr_0_after_write \(\) -> \[1, 63\] main::1::arr_1_after_write \(\) -> \[2, 63\] main::1::arr_2_after_write \(\) -> \[3, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc index 723c56de0f2..5f3509be976 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc @@ -3,8 +3,8 @@ main.c --dependence-graph-vs --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 0 \[in\]$ -^Data dependencies: 2 \[a\]$ -^Data dependencies: 2 \[a\], 9 \[a\]$ +^Data dependencies: 14 \[in\]$ +^Data dependencies: 16 \[a\]$ +^Data dependencies: 16 \[a\], 23 \[a\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc index 7eea9330446..a31862b882b 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc @@ -3,8 +3,8 @@ main.c --dependence-graph-vs --show -DINEQ ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 0 \[in\]$ -^Data dependencies: 2 \[a\]$ -^Data dependencies: 2 \[a\], 9 \[a\]$ +^Data dependencies: 14 \[in\]$ +^Data dependencies: 16 \[a\]$ +^Data dependencies: 16 \[a\], 23 \[a\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc index dbbefa74c2e..9ad3be927ed 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc @@ -3,24 +3,24 @@ main.c --no-standard-checks file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 48 \[st.a\]$ -^Data dependencies: 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ -^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ -^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 16 \[st.a\]$ +^Data dependencies: 16 \[st.b\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 47 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 46 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 48 \[arr\[(\([^)]*\))?2\]\], 50 \[arr\[(\([^)]*\))?2\]\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\], 66 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\], 69 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\], 66 \[st.a\], 69 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 19 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 22 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 19 \[ar\[(\([^)]*\))?0\]\], 22 \[ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc index 25369297c5f..6ff74a15be4 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc @@ -3,25 +3,25 @@ main.c --no-standard-checks file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 48 \[st.a\]$ -^Data dependencies: 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 6 \[out1\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ -^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ -^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 16 \[st.a\]$ +^Data dependencies: 16 \[st.b\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 34 \[out1\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 47 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 46 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 48 \[arr\[(\([^)]*\))?2\]\], 50 \[arr\[(\([^)]*\))?2\]\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\], 66 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\], 69 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\], 66 \[st.a\], 69 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 19 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 22 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 19 \[ar\[(\([^)]*\))?0\]\], 22 \[ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc index 1132fa4e2c1..969b8209866 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc @@ -6,5 +6,5 @@ activate-multi-line-match ^SIGNAL=0$ // Assignment from the result of a function call to a function with no body // should have a data dependency on the function -^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 := .*nondet.* +^Data dependencies: 18 \[f2\]\n(.*\n).*\/\/ 19 file .*main.c line 15 function main\n.*t2 := .*nondet.* -- diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index 0894cc0c9a5..a7244ea42d9 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc @@ -4,5 +4,5 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[(\([^)]*\))?i\]\], 2 \[g_a\[(\([^)]*\))?i\]\], 3 \[g_a\[(\([^)]*\))?i\]\], 7 \[g_a\[(\([^)]*\))?i\]\] +\*\*\*\* 23 file .*main\.c line 22 function main\nControl dependencies: 2 \[UNCONDITIONAL\]\nData dependencies: 15 \[g_a\[(\([^)]*\))?i\]\], 16 \[g_a\[(\([^)]*\))?i\]\], 17 \[g_a\[(\([^)]*\))?i\]\], 21 \[g_a\[(\([^)]*\))?i\]\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc index 6c77e6b6ad1..cd3b92417a2 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::z \(\) -> \[3, 3\] @ \[5\] +main::1::z \(\) -> \[3, 3\] @ \[19\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc index e9a42883da9..0251020135a 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc @@ -3,5 +3,5 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::z \(\) -> \[3, 4\] @ \[9\] +main::1::z \(\) -> \[3, 4\] @ \[23\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc index b72154af257..b43d9f59178 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a \(\) -> \[6, 6\] @ \[7\] +main::1::a \(\) -> \[6, 6\] @ \[21\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c index ab08a8125a1..602efb00786 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c @@ -1,6 +1,3 @@ -#include -#include - struct Vec2 { int x; diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc index 3550f5d1dc2..9250bb41e2c 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --vsd-structs every-field --vsd-pointers constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::vecMinusTenAndTen \(\) -> \{.x=\[FFFFFFF6, FFFFFFF6\] \@ \[3\], .y=\[A, A\] \@ \[3\]\} @ \[3\] -main::1::1::vecZero \(\) -> \{.x=\[0, 0\] \@ \[8\], .y=\[0, 0\] \@ \[8\]\} \@ \[8\] -main::1::2::vecOne \(\) -> \{.x=\[1, 1\] \@ \[13\], .y=\[1, 1\] \@ \[13\]\} \@ \[13\] -main::1::vecZeroOrOne \(\) -> \{.x=\[0, 1\] \@ \[17\], .y=\[0, 1\] \@ \[17\]\} \@ \[17\] -main::1::vecThirteenAndFourtyTwo \(\) -> \{.x=\[D, D\] \@ \[21\], .y=\[2A, 2A\] \@ \[21\]\} \@ \[21\] +main::1::vecMinusTenAndTen \(\) -> \{.x=\[FFFFFFF6, FFFFFFF6\] \@ \[23\], .y=\[A, A\] \@ \[23\]\} @ \[23\] +main::1::1::vecZero \(\) -> \{.x=\[0, 0\] \@ \[28\], .y=\[0, 0\] \@ \[28\]\} \@ \[28\] +main::1::2::vecOne \(\) -> \{.x=\[1, 1\] \@ \[33\], .y=\[1, 1\] \@ \[33\]\} \@ \[33\] +main::1::vecZeroOrOne \(\) -> \{.x=\[0, 1\] \@ \[37\], .y=\[0, 1\] \@ \[37\]\} \@ \[37\] +main::1::vecThirteenAndFourtyTwo \(\) -> \{.x=\[D, D\] \@ \[41\], .y=\[2A, 2A\] \@ \[41\]\} \@ \[41\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc index d57a6fc8571..db77d203e2d 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> \[1, 1\] @ \[2\] -main::1::b2 \(\) -> \[0, 0\] @ \[3\] -main::1::i \(\) -> \[A\, 14\] @ \[11\] +main::1::b1 \(\) -> \[1, 1\] @ \[17\] +main::1::b2 \(\) -> \[0, 0\] @ \[18\] +main::1::i \(\) -> \[A\, 14\] @ \[26\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc index 3698a50632e..3b1bf2db873 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::r \(\) -> TOP @ \[1\] -main::1::s \(\) -> \[0, 0\] @ \[3\] +main::1::r \(\) -> TOP @ \[13\] +main::1::s \(\) -> \[0, 0\] @ \[15\] diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc index b648080c3a6..51673e04be8 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::r \(\) -> \[2, 2\] @ \[1\] -main::1::s \(\) -> \[3, 3\] @ \[3\] -main::1::t \(\) -> \[4, 4\] @ \[5\] -main::1::x \(\) -> \[9, 9\] @ \[7\] -main::1::y \(\) -> \[C, C\] @ \[9\] -main::1::z \(\) -> \[18, 18\] @ \[11\] +main::1::r \(\) -> \[2, 2\] @ \[12\] +main::1::s \(\) -> \[3, 3\] @ \[14\] +main::1::t \(\) -> \[4, 4\] @ \[16\] +main::1::x \(\) -> \[9, 9\] @ \[18\] +main::1::y \(\) -> \[C, C\] @ \[20\] +main::1::z \(\) -> \[18, 18\] @ \[22\] diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc index 7fdf22da114..b4dcf5cd19d 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::zero \(\) -> \[0, 0\] @ \[3\] -main::1::1::one \(\) -> \[1, 1\] @ \[8\] -main::1::2::minus_one \(\) -> \[FFFFFFFF, FFFFFFFF\] @ \[13\] -main::1::between_minus_one_and_one \(\) -> \[FFFFFFFF, 1\] @ \[17\] -main::1::thirteen \(\) -> \[D, D\] @ \[20\] +main::1::zero \(\) -> \[0, 0\] @ \[17\] +main::1::1::one \(\) -> \[1, 1\] @ \[22\] +main::1::2::minus_one \(\) -> \[FFFFFFFF, FFFFFFFF\] @ \[27\] +main::1::between_minus_one_and_one \(\) -> \[FFFFFFFF, 1\] @ \[31\] +main::1::thirteen \(\) -> \[D, D\] @ \[34\] -- diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc index 5f817b5fb71..4d773713b38 100644 --- a/regression/goto-harness/havoc-global-int-01/test.desc +++ b/regression/goto-harness/havoc-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 --havoc-variables x +--harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:13 --havoc-variables x ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc index fe3abf4614d..8665faa2ddc 100644 --- a/regression/goto-harness/havoc-global-int-02/test.desc +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:70 --havoc-variables y ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ ^EXIT=10$ diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc index acea3f2c367..bed2dded6de 100644 --- a/regression/goto-harness/havoc-global-struct/test.desc +++ b/regression/goto-harness/havoc-global-struct/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:18 --havoc-variables simple ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$ diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc index aabcd925525..af82f5acc82 100644 --- a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:15 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc index b9be03e032d..03ab6a5fcc2 100644 --- a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:13 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc index cbfab21c496..8b7ec7ceb12 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:13 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc index 255126954dc..8ca8647dbf1 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:14 ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc index cbfab21c496..af82f5acc82 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:15 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc index aabcd925525..de661b408a0 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:14 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc index db09a8df0fb..83b8203e471 100644 --- a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 _ --no-standard-checks +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:14 _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c index 4f09cb9f5a9..1271e86e789 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; do diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc index 66901d97a73..171ee41aef1 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc index 35461234741..709ed590b4e 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c index 4650b9eb088..75bfa7d20a9 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { for(int i = 0; i < 10; ++i) { diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc index 6a1ece48341..b3724408c07 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc index 2e65bcfde15..d391b71b2fd 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c index 317add397f5..15da3bcef76 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc index ed29c69fe63..9ddcaa4c5af 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc @@ -1,7 +1,7 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \} -^12 is head of \{ 12, 13, 14, 15, 16, 17, 18 \(backedge\) \} +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \} +^24 is head of \{ 24, 25, 26, 27, 28, 29, 30 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc index 2c0f0be7f8c..9fe26dbb479 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc @@ -1,7 +1,7 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \} -^11 is head of \{ 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \} +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 19 \(backedge\) \} +^23 is head of \{ 23, 24 \(backedge\), 25, 26, 27, 28 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c index 3351d7924f9..cf909c7aa2c 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc index 42c1a2014e2..f8e2f26be19 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc index bda65fab1af..75c18d0c4d7 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6 \(backedge\), 7, 8, 9 \(backedge\), 10, 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18 \(backedge\), 19, 20, 21 \(backedge\), 22, 23, 24 \(backedge\), 25, 26, 27, 28 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c index c789a6e7959..46daaca17a6 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc index a3b48510cc8..a69cd7fffdd 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 10, 11, 12 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc index 7c5191bd44c..aa813b94a4c 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 10, 11, 12 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c index 0e261f47c6e..19a11836944 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc index 45ff24304fe..e41e7c63275 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc index 43ded7de7dd..54bb29d40aa 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc index 4df83b91759..61c85917287 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc @@ -1,7 +1,7 @@ CORE main.c --ensure-one-backedge-per-target --show-lexical-loops -^3 is head of \{ 3, 4, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26 \(backedge\) \}$ -^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ +^15 is head of \{ 15, 16, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38 \(backedge\) \}$ +^29 is head of \{ 29, 30, 34, 35, 36, 37 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc index 3c75bba4947..818f705f11e 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc @@ -1,7 +1,7 @@ CORE main.c --show-lexical-loops -^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ +^29 is head of \{ 29, 30, 34, 35, 36, 37 \(backedge\) \}$ Note not all loops were in lexical loop form ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c index 53e212b6d25..868704603a3 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; while(i < 10) diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc index 45ff24304fe..e41e7c63275 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc index 484ed113649..8605e4e0670 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/lexical-loops1/test.c b/regression/goto-instrument/lexical-loops1/test.c index 9b775114782..0fd0838cfbb 100644 --- a/regression/goto-instrument/lexical-loops1/test.c +++ b/regression/goto-instrument/lexical-loops1/test.c @@ -1,10 +1,10 @@ - -int main(int argc, char **argv) +int main() { + int count; for(int i = 0; i < 10; ++i) { - ++argc; + ++count; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops1/test.desc b/regression/goto-instrument/lexical-loops1/test.desc index 583dfadccd5..c92f53ec835 100644 --- a/regression/goto-instrument/lexical-loops1/test.desc +++ b/regression/goto-instrument/lexical-loops1/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops _ --no-standard-checks -2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +15 is head of \{ 15, 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops2/test.c b/regression/goto-instrument/lexical-loops2/test.c index ec4744ac62b..2bf3d08de6e 100644 --- a/regression/goto-instrument/lexical-loops2/test.c +++ b/regression/goto-instrument/lexical-loops2/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); while(i < 10) { ++i; - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops2/test.desc b/regression/goto-instrument/lexical-loops2/test.desc index 17557991dc3..77fb1102f40 100644 --- a/regression/goto-instrument/lexical-loops2/test.desc +++ b/regression/goto-instrument/lexical-loops2/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +16 is head of \{ 16, 17, 18, 19 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops3/test.c b/regression/goto-instrument/lexical-loops3/test.c index 56cfe344e48..9c340cdddf7 100644 --- a/regression/goto-instrument/lexical-loops3/test.c +++ b/regression/goto-instrument/lexical-loops3/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); do { ++i; - argc--; + count--; } while(i < 10); - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops3/test.desc b/regression/goto-instrument/lexical-loops3/test.desc index 424b8612b7e..94be50cd2c7 100644 --- a/regression/goto-instrument/lexical-loops3/test.desc +++ b/regression/goto-instrument/lexical-loops3/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4 \(backedge\) \} +16 is head of \{ 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops4/test.c b/regression/goto-instrument/lexical-loops4/test.c index 46299288377..820ce39a9b1 100644 --- a/regression/goto-instrument/lexical-loops4/test.c +++ b/regression/goto-instrument/lexical-loops4/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); head: ++i; - argc--; + count--; if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops4/test.desc b/regression/goto-instrument/lexical-loops4/test.desc index 424b8612b7e..94be50cd2c7 100644 --- a/regression/goto-instrument/lexical-loops4/test.desc +++ b/regression/goto-instrument/lexical-loops4/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4 \(backedge\) \} +16 is head of \{ 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops5/test.c b/regression/goto-instrument/lexical-loops5/test.c index f9bb65549e2..07af6f1f598 100644 --- a/regression/goto-instrument/lexical-loops5/test.c +++ b/regression/goto-instrument/lexical-loops5/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { + int count; + for(int i = 0; i < 5; ++i) { for(int j = 0; j < 5; ++j) { - argc++; + count++; } } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops5/test.desc b/regression/goto-instrument/lexical-loops5/test.desc index 8e2895aa5f1..dd3828d77ee 100644 --- a/regression/goto-instrument/lexical-loops5/test.desc +++ b/regression/goto-instrument/lexical-loops5/test.desc @@ -1,8 +1,8 @@ CORE test.c --show-lexical-loops _ --no-standard-checks -2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 \(backedge\) \} -5 is head of \{ 5, 6, 7, 8 \(backedge\) \} +15 is head of \{ 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 \(backedge\) \} +18 is head of \{ 18, 19, 20, 21 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops6/test.c b/regression/goto-instrument/lexical-loops6/test.c index bdb466108da..7c90c44467f 100644 --- a/regression/goto-instrument/lexical-loops6/test.c +++ b/regression/goto-instrument/lexical-loops6/test.c @@ -1,17 +1,18 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); - if(argc % 2) + if(count % 2) goto head2; head: - argc--; + count--; head2: ++i; if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops7/test.c b/regression/goto-instrument/lexical-loops7/test.c index 7332dcf7d88..ea1ea7e722c 100644 --- a/regression/goto-instrument/lexical-loops7/test.c +++ b/regression/goto-instrument/lexical-loops7/test.c @@ -1,15 +1,16 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); head: - argc--; + count--; ++i; if(i < 10 && i % 2) goto head; else if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops7/test.desc b/regression/goto-instrument/lexical-loops7/test.desc index f2facf040b6..a83e70cf31a 100644 --- a/regression/goto-instrument/lexical-loops7/test.desc +++ b/regression/goto-instrument/lexical-loops7/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-lexical-loops ^Note not all loops were in lexical loop form$ -^2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +^16 is head of \{ 16, 17, 18, 19 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops8/test.c b/regression/goto-instrument/lexical-loops8/test.c index d7a4a1159ad..9fd38163fdb 100644 --- a/regression/goto-instrument/lexical-loops8/test.c +++ b/regression/goto-instrument/lexical-loops8/test.c @@ -1,17 +1,17 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; while(i < 10) { - if(argc == 5) + if(count == 5) break; ++i; - if(argc % 7) + if(count % 7) continue; - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops8/test.desc b/regression/goto-instrument/lexical-loops8/test.desc index b7e69cb2d8f..15c773844bd 100644 --- a/regression/goto-instrument/lexical-loops8/test.desc +++ b/regression/goto-instrument/lexical-loops8/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 \(backedge\) \}$ +^15 is head of \{ 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops9/test.c b/regression/goto-instrument/lexical-loops9/test.c index 96ba286ae01..7eded758356 100644 --- a/regression/goto-instrument/lexical-loops9/test.c +++ b/regression/goto-instrument/lexical-loops9/test.c @@ -1,18 +1,19 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 5); while(i < 10) { ++i; - if(argc == 5) + if(count == 5) { ++i; break; } - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops9/test.desc b/regression/goto-instrument/lexical-loops9/test.desc index 34316088040..1ab01bc9a98 100644 --- a/regression/goto-instrument/lexical-loops9/test.desc +++ b/regression/goto-instrument/lexical-loops9/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -^2 is head of \{ 2, 3, 4, 7, 8, 9 \(backedge\) \}$ +^16 is head of \{ 16, 17, 18, 21, 22, 23 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/natural-loops-multiple-backedges/main.c b/regression/goto-instrument/natural-loops-multiple-backedges/main.c index d78adfa9ae5..e70523e0688 100644 --- a/regression/goto-instrument/natural-loops-multiple-backedges/main.c +++ b/regression/goto-instrument/natural-loops-multiple-backedges/main.c @@ -1,10 +1,12 @@ -int main(int argc, char **argv) +int main() { + int count; + __CPROVER_assume(count > 0); loop_header: - --argc; - if(argc == 1) + --count; + if(count == 1) goto loop_header; - else if(argc == 2) + else if(count == 2) goto loop_header; - return argc; + return count; } diff --git a/regression/goto-instrument/natural-loops-multiple-backedges/test.desc b/regression/goto-instrument/natural-loops-multiple-backedges/test.desc index 93c1bd15961..19f0f3ba402 100644 --- a/regression/goto-instrument/natural-loops-multiple-backedges/test.desc +++ b/regression/goto-instrument/natural-loops-multiple-backedges/test.desc @@ -1,11 +1,11 @@ CORE main.c --show-natural-loops -0 is head of \{ 0, 1, 2 \(backedge\), 4 \(backedge\) \} +14 is head of \{ 14, 15, 16 \(backedge\), 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -In the line beginning "0 is head of" we expect to get 0, 1, 2 and 4 in some -order +In the line beginning "14 is head of" we expect to get 14, 15, 16 and 18 in some +order. diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index f4ac42e6d4a..1a53300f444 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -21,10 +21,11 @@ Date: June 2003 void goto_functionst::compute_location_numbers() { unused_location_number = 0; - for(auto &func : function_map) + auto sorted_funcs = sorted(); + for(auto &it : sorted_funcs) { // Side-effect: bumps unused_location_number. - func.second.body.compute_location_numbers(unused_location_number); + it->second.body.compute_location_numbers(unused_location_number); } } From 5072fbe222d0906c72e23a1588a95e6e124383ad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Jan 2026 19:29:00 +0000 Subject: [PATCH 7/8] Make property numbering and show-properties fully deterministic Use lexicographic ordering when iterating over goto functions to avoid property numbers (or the order in which they printed) to depend on hash values. --- src/goto-programs/set_properties.cpp | 6 ++---- src/goto-programs/show_properties.cpp | 14 ++++++++++---- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 49a5d18dfbe..6c122801668 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -131,9 +131,7 @@ void label_properties(goto_functionst &goto_functions) { std::map property_counters; - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + auto sorted = goto_functions.sorted(); + for(auto &it : sorted) label_properties(it->first, it->second.body, property_counters); } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index c3e94c26600..38e46131f50 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -180,8 +180,10 @@ void show_properties_json( messaget msg(message_handler); json_arrayt json_properties; - for(const auto &fct : goto_functions.function_map) - convert_properties_json(json_properties, ns, fct.first, fct.second.body); + // sort alphabetically + const auto sorted = goto_functions.sorted(); + for(const auto &it : sorted) + convert_properties_json(json_properties, ns, it->first, it->second.body); json_objectt json_result{{"properties", json_properties}}; msg.result() << json_result; @@ -196,8 +198,12 @@ void show_properties( if(ui == ui_message_handlert::uit::JSON_UI) show_properties_json(ns, ui_message_handler, goto_functions); else - for(const auto &fct : goto_functions.function_map) - show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body); + { + // sort alphabetically + const auto sorted = goto_functions.sorted(); + for(const auto &it : sorted) + show_properties(ns, it->first, ui_message_handler, ui, it->second.body); + } } void show_properties( From 37f2da4d6e2e2646fdd3190949bb68c28612e6d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 28 Jan 2026 11:25:09 +0000 Subject: [PATCH 8/8] Simplify pointer casts of pointer arithmetic This permits simplifying, e.g., `(char*)(ptr + 1) + -1` to `(char*)ptr` when `ptr` is `unsigned char*`. This, in turn, avoids different formulae produced on AArch64 (where `char` is unsigned) and Apple Silicon/macOS (where `char` is signed, as is the case on x86). --- src/util/simplify_expr.cpp | 39 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 8670a17b974..283022f02a6 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1012,6 +1012,45 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) } } + // Push a pointer typecast into pointer arithmetic + // (T)(ptr + int) ---> (T)ptr + sizeof(inner-st)/sizeof(outer-st)*int + // when the inner subtype's size is a multiple of the outer subtype's size + if( + expr_type.id() == ID_pointer && op_type.id() == ID_pointer && + expr.op().id() == ID_plus) + { + const auto step = + pointer_offset_size(to_pointer_type(op_type).base_type(), ns); + const auto new_step = + pointer_offset_size(to_pointer_type(expr_type).base_type(), ns); + + if( + step.has_value() && *step != 0 && new_step.has_value() && + *new_step != 0 && *step >= *new_step && *step % *new_step == 0) + { + const typet size_t_type(size_type()); + auto new_expr = expr.op(); + new_expr.type() = expr.type(); + + for(auto &op : new_expr.operands()) + { + if(op.type().id() == ID_pointer) + { + exprt new_op = simplify_typecast(typecast_exprt{op, expr.type()}); + op = std::move(new_op); + } + else if(*step > *new_step) + { + exprt new_op = simplify_mult( + mult_exprt{from_integer(*step / *new_step, op.type()), op}); + op = std::move(new_op); + } + } + + return changed(simplify_plus(to_plus_expr(new_expr))); + } + } + const irep_idt &expr_type_id=expr_type.id(); const exprt &operand = expr.op(); const irep_idt &op_type_id=op_type.id();