From a531153b38ea5ec4a27ae8a1edc239108d0255c4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Jan 2022 14:24:14 +0000 Subject: [PATCH 1/6] CBMC library regression tests: ensure GNUC-only declarations are present MSVC won't have the built-in declarations available, and will thus fail type checking. --- regression/cbmc-library/__atomic_always_lock_free-01/main.c | 4 ++++ regression/cbmc-library/__atomic_clear-01/main.c | 4 ++++ regression/cbmc-library/__atomic_is_lock_free-01/main.c | 4 ++++ regression/cbmc-library/__atomic_signal_fence-01/main.c | 4 ++++ regression/cbmc-library/__atomic_test_and_set-01/main.c | 4 ++++ regression/cbmc-library/__atomic_thread_fence-01/main.c | 4 ++++ regression/cbmc-library/_longjmp-01/main.c | 4 ++++ regression/cbmc-library/_longjmp-01/test.desc | 4 ++-- 8 files changed, 30 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/main.c b/regression/cbmc-library/__atomic_always_lock_free-01/main.c index cfb762868e4..5b88bd587df 100644 --- a/regression/cbmc-library/__atomic_always_lock_free-01/main.c +++ b/regression/cbmc-library/__atomic_always_lock_free-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_always_lock_free(__CPROVER_size_t, void *); +#endif + int main() { assert(__atomic_always_lock_free(sizeof(int), 0)); diff --git a/regression/cbmc-library/__atomic_clear-01/main.c b/regression/cbmc-library/__atomic_clear-01/main.c index 94a759177c5..57bf57abbc2 100644 --- a/regression/cbmc-library/__atomic_clear-01/main.c +++ b/regression/cbmc-library/__atomic_clear-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_clear(_Bool *, int); +#endif + int main() { _Bool n; diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/main.c b/regression/cbmc-library/__atomic_is_lock_free-01/main.c index 514abeaac5d..3ac747b7976 100644 --- a/regression/cbmc-library/__atomic_is_lock_free-01/main.c +++ b/regression/cbmc-library/__atomic_is_lock_free-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_is_lock_free(__CPROVER_size_t, void *); +#endif + int main() { assert(__atomic_is_lock_free(sizeof(int), 0)); diff --git a/regression/cbmc-library/__atomic_signal_fence-01/main.c b/regression/cbmc-library/__atomic_signal_fence-01/main.c index 3a809cf651f..539a54287e5 100644 --- a/regression/cbmc-library/__atomic_signal_fence-01/main.c +++ b/regression/cbmc-library/__atomic_signal_fence-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_signal_fence(int); +#endif + int main() { __atomic_signal_fence(0); diff --git a/regression/cbmc-library/__atomic_test_and_set-01/main.c b/regression/cbmc-library/__atomic_test_and_set-01/main.c index 9a9150b3766..4fdcf0ffb68 100644 --- a/regression/cbmc-library/__atomic_test_and_set-01/main.c +++ b/regression/cbmc-library/__atomic_test_and_set-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_test_and_set(void *, int); +#endif + int main() { char c = 0; diff --git a/regression/cbmc-library/__atomic_thread_fence-01/main.c b/regression/cbmc-library/__atomic_thread_fence-01/main.c index b9001b81810..dd08b8e1801 100644 --- a/regression/cbmc-library/__atomic_thread_fence-01/main.c +++ b/regression/cbmc-library/__atomic_thread_fence-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_thread_fence(int); +#endif + int main() { __atomic_thread_fence(0); diff --git a/regression/cbmc-library/_longjmp-01/main.c b/regression/cbmc-library/_longjmp-01/main.c index cdac71afdc5..5be8777c4ed 100644 --- a/regression/cbmc-library/_longjmp-01/main.c +++ b/regression/cbmc-library/_longjmp-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +# define _longjmp(a, b) longjmp(a, b) +#endif + static jmp_buf env; int main() diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/regression/cbmc-library/_longjmp-01/test.desc index c07910fc69d..b7d7e2001ce 100644 --- a/regression/cbmc-library/_longjmp-01/test.desc +++ b/regression/cbmc-library/_longjmp-01/test.desc @@ -1,8 +1,8 @@ CORE main.c --pointer-check --bounds-check -^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$ -^\[main.assertion.1\] line 8 unreachable: SUCCESS$ +^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$ +^\[main.assertion.1\] line 12 unreachable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ From 70650347fbff47ecee68c4c796c6a030767cabd3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Jan 2022 14:50:03 +0000 Subject: [PATCH 2/6] enum-trace1 regression test: ensure inputs are sane The test descriptions expect valid enum values, which we didn't actually have any guarantee built into the test for. --- regression/cbmc/enum-trace1/main.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/regression/cbmc/enum-trace1/main.c b/regression/cbmc/enum-trace1/main.c index b4e8ce48d74..2256efc27c1 100644 --- a/regression/cbmc/enum-trace1/main.c +++ b/regression/cbmc/enum-trace1/main.c @@ -16,6 +16,9 @@ typedef enum ENUMT void test(enum ENUM e, enum_t t) { + // ensure sane input values + __CPROVER_assume(__CPROVER_enum_is_in_range(e)); + __CPROVER_assume(__CPROVER_enum_is_in_range(t)); enum ENUM ee = e; enum_t tt = t; From 7f1cc0f2055f3db8ce3cc5eec805f43fa96c0dfa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 28 Feb 2019 10:57:37 +0000 Subject: [PATCH 3/6] Use the linker when adding library functions This enables type checking of missing functions vs library-provided functions, and also enables type sanitisation as done by the linker. Co-authored-by: Peter Schrammel --- .../cbmc-library/__errno_location-01/main.c | 6 +- .../__errno_location-01/test.desc | 2 +- regression/cbmc-library/memcpy-07/main.c | 1 + .../String_Abstraction17/strcpy-no-decl.c | 3 +- .../cbmc/String_Abstraction17/test.desc | 10 +- .../s2n_hash_inlined.c | 2 + src/ansi-c/cprover_library.cpp | 5 +- src/ansi-c/cprover_library.h | 1 + src/cpp/cprover_library.cpp | 5 +- src/cpp/cprover_library.h | 1 + src/goto-programs/link_to_library.cpp | 134 ++++++++++++++---- src/goto-programs/link_to_library.h | 7 +- 12 files changed, 133 insertions(+), 44 deletions(-) diff --git a/regression/cbmc-library/__errno_location-01/main.c b/regression/cbmc-library/__errno_location-01/main.c index 24329d09ff5..c32d17bf73b 100644 --- a/regression/cbmc-library/__errno_location-01/main.c +++ b/regression/cbmc-library/__errno_location-01/main.c @@ -1,9 +1,9 @@ #include #include -int main() +int main(int arc, char *argv[]) { - __errno_location(); - assert(0); + // errno expands to use of __errno_location() with glibc + assert(errno == 0); return 0; } diff --git a/regression/cbmc-library/__errno_location-01/test.desc b/regression/cbmc-library/__errno_location-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/__errno_location-01/test.desc +++ b/regression/cbmc-library/__errno_location-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/memcpy-07/main.c b/regression/cbmc-library/memcpy-07/main.c index 06ad39e2b74..971509901fc 100644 --- a/regression/cbmc-library/memcpy-07/main.c +++ b/regression/cbmc-library/memcpy-07/main.c @@ -1,4 +1,5 @@ // #include intentionally omitted +void *memcpy(); struct c { diff --git a/regression/cbmc/String_Abstraction17/strcpy-no-decl.c b/regression/cbmc/String_Abstraction17/strcpy-no-decl.c index 0e7a93df5e6..17c80a7a2d5 100644 --- a/regression/cbmc/String_Abstraction17/strcpy-no-decl.c +++ b/regression/cbmc/String_Abstraction17/strcpy-no-decl.c @@ -1,4 +1,5 @@ -void *malloc(unsigned); +#include +// string.h intentionally omitted char *make_str() { diff --git a/regression/cbmc/String_Abstraction17/test.desc b/regression/cbmc/String_Abstraction17/test.desc index ea2896bae68..ad0106474bd 100644 --- a/regression/cbmc/String_Abstraction17/test.desc +++ b/regression/cbmc/String_Abstraction17/test.desc @@ -1,11 +1,13 @@ CORE strcpy-no-decl.c --string-abstraction --validate-goto-model -Condition: strlen type inconsistency -^EXIT=(127|134)$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -While this test currently passes when omitting --validate-goto-model, we should -expect a report of type inconsistencies as no forward declarations are present. +The linker is able to fix up type inconsistencies of the missing function +declarations, but the absence of a declaration of strlen results in not picking +up the library model. Consequently the assumption does not work as intended, and +verification fails. Adding #include makes verification pass as +expected. diff --git a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c index 5dc784acc4a..0c4baffd118 100644 --- a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c +++ b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c @@ -1,3 +1,5 @@ +#include + // This file is highly reduced from some open source projects. // The following four lines are adapted from the openssl library // Full repository here: diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 6582a491b1e..9966e83e669 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -98,7 +98,8 @@ std::string get_cprover_library_text( void cprover_c_library_factory( const std::set &functions, - symbol_table_baset &symbol_table, + const symbol_table_baset &symbol_table, + symbol_table_baset &dest_symbol_table, message_handlert &message_handler) { if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE) @@ -107,7 +108,7 @@ void cprover_c_library_factory( std::string library_text = get_cprover_library_text(functions, symbol_table, false); - add_library(library_text, symbol_table, message_handler); + add_library(library_text, dest_symbol_table, message_handler); } void add_library( diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index 80bbfea2608..33c67d980ad 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -41,6 +41,7 @@ void add_library( void cprover_c_library_factory( const std::set &functions, + const symbol_table_baset &, symbol_table_baset &, message_handlert &); diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp index e906808b4ec..b79134b37cb 100644 --- a/src/cpp/cprover_library.cpp +++ b/src/cpp/cprover_library.cpp @@ -37,7 +37,8 @@ static std::string get_cprover_library_text( void cprover_cpp_library_factory( const std::set &functions, - symbol_table_baset &symbol_table, + const symbol_table_baset &symbol_table, + symbol_table_baset &dest_symbol_table, message_handlert &message_handler) { if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE) @@ -46,5 +47,5 @@ void cprover_cpp_library_factory( const std::string library_text = get_cprover_library_text(functions, symbol_table); - add_library(library_text, symbol_table, message_handler); + add_library(library_text, dest_symbol_table, message_handler); } diff --git a/src/cpp/cprover_library.h b/src/cpp/cprover_library.h index 54a5661aec5..6000972eb23 100644 --- a/src/cpp/cprover_library.h +++ b/src/cpp/cprover_library.h @@ -18,6 +18,7 @@ class symbol_table_baset; void cprover_cpp_library_factory( const std::set &functions, + const symbol_table_baset &, symbol_table_baset &, message_handlert &); diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 48b18553bb5..2e656cf589f 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -11,38 +11,100 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_to_library.h" +#include + #include "compute_called_functions.h" #include "goto_convert_functions.h" #include "goto_model.h" +#include "link_goto_model.h" + +/// Try to add \p missing_function from \p library to \p goto_model. +static optionalt add_one_function( + goto_modelt &goto_model, + message_handlert &message_handler, + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &library, + const irep_idt &missing_function) +{ + goto_modelt library_model; + library( + {missing_function}, + goto_model.symbol_table, + library_model.symbol_table, + message_handler); + + // convert to CFG + if( + library_model.symbol_table.symbols.find(missing_function) != + library_model.symbol_table.symbols.end()) + { + goto_convert( + missing_function, + library_model.symbol_table, + library_model.goto_functions, + message_handler); + } + + // check whether additional initialization may be required + if( + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != + goto_model.goto_functions.function_map.end()) + { + for(const auto &entry : library_model.symbol_table) + { + if( + entry.second.is_static_lifetime && !entry.second.is_type && + !entry.second.is_macro && entry.second.type.id() != ID_code && + !goto_model.symbol_table.has_symbol(entry.first)) + { + goto_model.unload(INITIALIZE_FUNCTION); + break; + } + } + } + + return link_goto_model(goto_model, std::move(library_model), message_handler); +} /// Complete missing function definitions using the \p library. /// \param goto_model: goto model that may contain function calls and symbols /// with missing function bodies /// \param message_handler: message handler to report library processing /// problems -/// \param library: generator function that produces function definitions for a -/// given set of symbol names that have no body. +/// \param library: generator function that produces function definitions (in +/// the symbol table that is the third parameter) for a given set of symbol +/// names (first parameter) that have no body in the source symbol table +/// (second parameter). void link_to_library( goto_modelt &goto_model, message_handlert &message_handler, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> - &library) + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &library) { // this needs a fixedpoint, as library functions // may depend on other library functions std::set added_functions; + // Linking in library functions (now seeing full definitions rather than + // forward declarations, or perhaps even cases of missing forward + // declarations) may result in type changes to objects. + replace_symbolt::expr_mapt object_type_updates; + const bool had_init = + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != + goto_model.goto_functions.function_map.end(); while(true) { std::unordered_set called_functions = compute_called_functions(goto_model.goto_functions); - // eliminate those for which we already have a body - - std::set missing_functions; - + bool changed = false; for(const auto &id : called_functions) { goto_functionst::function_mapt::const_iterator f_it = @@ -59,30 +121,44 @@ void link_to_library( // already added } else - missing_functions.insert(id); + { + changed = true; + added_functions.insert(id); + + auto updates_opt = + add_one_function(goto_model, message_handler, library, id); + if(!updates_opt.has_value()) + { + messaget log{message_handler}; + log.warning() << "Linking library function '" << id << "' failed" + << messaget::eom; + continue; + } + object_type_updates.insert(updates_opt->begin(), updates_opt->end()); + } } // done? - if(missing_functions.empty()) + if(!changed) break; + } - library(missing_functions, goto_model.symbol_table, message_handler); - - // convert to CFG - for(const auto &id : missing_functions) - { - if( - goto_model.symbol_table.symbols.find(id) != - goto_model.symbol_table.symbols.end()) - { - goto_convert( - id, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - } - - added_functions.insert(id); - } + if( + had_init && + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) == + goto_model.goto_functions.function_map.end()) + { + static_lifetime_init( + goto_model.symbol_table, + goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); + goto_convert( + INITIALIZE_FUNCTION, + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); + goto_model.goto_functions.update(); } + + if(!object_type_updates.empty()) + finalize_linking(goto_model, object_type_updates); } diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h index 8f04f377ddc..8ddf2d3b0b8 100644 --- a/src/goto-programs/link_to_library.h +++ b/src/goto-programs/link_to_library.h @@ -24,7 +24,10 @@ class symbol_tablet; void link_to_library( goto_modelt &, message_handlert &, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> &); + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &); #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H From 5f7e0ded56e28051f2d5a591caf16fe2261d2f5b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 17 Jan 2022 21:07:00 +0000 Subject: [PATCH 4/6] C library: move pipe() related definitions to library With the support of building initialisers while adding the library we can move library-only symbols to the library. This avoids polluting the initialisation function for all cases that don't actually use pipe-related library functions. --- regression/cprover/arrays/array1.desc | 10 +-- regression/cprover/arrays/array2.desc | 6 +- regression/cprover/basic/assume1.desc | 6 +- regression/cprover/basic/basic1.desc | 6 +- regression/cprover/basic/basic2.desc | 10 +-- regression/cprover/basic/basic3.desc | 10 +-- regression/cprover/basic/basic4.desc | 8 +-- regression/cprover/basic/basic5.desc | 12 ++-- regression/cprover/basic/basic6.desc | 6 +- regression/cprover/basic/nondet1.desc | 14 ++--- regression/cprover/branching/branching1.desc | 24 ++++---- regression/cprover/branching/branching2.desc | 16 ++--- regression/cprover/float/basic-float1.desc | 4 +- .../cprover/function_calls/call_no_body1.desc | 4 +- .../cprover/function_calls/call_no_body2.desc | 2 +- regression/cprover/loops/do_while1.desc | 12 ++-- regression/cprover/loops/for1.desc | 16 ++--- regression/cprover/loops/for2.desc | 12 ++-- regression/cprover/loops/while-break1.desc | 18 +++--- regression/cprover/pointers/malloc1.desc | 2 +- regression/cprover/pointers/pointers0.desc | 4 +- regression/cprover/pointers/pointers1.desc | 8 +-- regression/cprover/pointers/pointers2.desc | 12 ++-- regression/cprover/pointers/pointers3.desc | 4 +- regression/cprover/pointers/pointers4.desc | 8 +-- regression/cprover/pointers/pointers5.desc | 4 +- regression/cprover/pointers/pointers6.desc | 8 +-- regression/cprover/pointers/pointers7.desc | 16 ++--- regression/cprover/pointers/pointers8.desc | 6 +- regression/cprover/pointers/pointers9.desc | 8 +-- .../cprover/pointers/struct_pointer1.desc | 6 +- .../cprover/pointers/struct_pointer2.desc | 6 +- .../cprover/safety/use_after_free1.desc | 4 +- .../cprover/structs/nondet_struct1.desc | 2 +- regression/cprover/structs/struct1.desc | 4 +- regression/cprover/structs/struct2.desc | 8 +-- .../constant_propagation_01/test-vsd.desc | 2 +- .../constant_propagation_01/test.desc | 2 +- .../constant_propagation_02/test-vsd.desc | 2 +- .../constant_propagation_02/test.desc | 2 +- .../constant_propagation_03/test-vsd.desc | 2 +- .../constant_propagation_03/test.desc | 2 +- .../constant_propagation_04/test-vsd.desc | 2 +- .../constant_propagation_04/test.desc | 2 +- .../constant_propagation_07/test-vsd.desc | 2 +- .../constant_propagation_07/test.desc | 2 +- .../constant_propagation_08/test-vsd.desc | 2 +- .../constant_propagation_11/test-vsd.desc | 2 +- .../constant_propagation_11/test.desc | 2 +- .../constant_propagation_12/test-vsd.desc | 2 +- .../constant_propagation_12/test.desc | 2 +- .../test-liveness-show.desc | 4 +- .../test-liveness-three-way-show.desc | 4 +- .../test-write-location-show.desc | 2 +- .../test-write-location-three-way-show.desc | 2 +- .../test.desc | 45 +++++++------- .../test.desc | 43 +++++++------ .../test.desc | 53 ++++++++-------- .../test.desc | 61 +++++++++---------- .../test.desc | 6 +- .../test.desc | 32 +++++----- .../test.desc | 32 +++++----- .../test.desc | 2 +- src/ansi-c/ansi_c_internal_additions.cpp | 5 -- src/ansi-c/library/cprover.h | 2 + src/ansi-c/library/unistd.c | 10 +-- src/cpp/cpp_internal_additions.cpp | 5 -- 67 files changed, 316 insertions(+), 328 deletions(-) diff --git a/regression/cprover/arrays/array1.desc b/regression/cprover/arrays/array1.desc index 896115d8009..c191c70855d 100644 --- a/regression/cprover/arrays/array1.desc +++ b/regression/cprover/arrays/array1.desc @@ -3,11 +3,11 @@ array1.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$ ^\[main\.assertion\.3\] line \d+ property 3: REFUTED$ diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc index 75f86008155..db7db1faf42 100644 --- a/regression/cprover/arrays/array2.desc +++ b/regression/cprover/arrays/array2.desc @@ -3,9 +3,9 @@ array2.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$ +^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S23\(ς\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/assume1.desc b/regression/cprover/basic/assume1.desc index 9ce490abc7c..7efdc15e8e2 100644 --- a/regression/cprover/basic/assume1.desc +++ b/regression/cprover/basic/assume1.desc @@ -6,9 +6,9 @@ assume1.c ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$ ^ \(\d+\) S0 = SInitial$ ^ \(\d+\) S1 = S0$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$ +^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S20\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/basic1.desc b/regression/cprover/basic/basic1.desc index 11a7b0ad24c..43759960f6d 100644 --- a/regression/cprover/basic/basic1.desc +++ b/regression/cprover/basic/basic1.desc @@ -5,8 +5,8 @@ basic1.c ^SIGNAL=0$ ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$ ^ \(\d+\) S0 = SInitial$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic2.desc b/regression/cprover/basic/basic2.desc index 297a94c2fc5..5ad0beb9fb1 100644 --- a/regression/cprover/basic/basic2.desc +++ b/regression/cprover/basic/basic2.desc @@ -3,11 +3,11 @@ basic2.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ +^\(\d+\) S18 = S17$ ^\(\d+\) S19 = S18$ -^\(\d+\) S20 = S19$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$ -^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic3.desc b/regression/cprover/basic/basic3.desc index eb2127fbc7b..f49ba79b237 100644 --- a/regression/cprover/basic/basic3.desc +++ b/regression/cprover/basic/basic3.desc @@ -3,10 +3,10 @@ basic3.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\) -\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\) -\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\) -\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\) -\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\) +\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\) +\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝y❞:=0\]\) +\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\) +\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝y❞:=2\]\) +\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\) ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic4.desc b/regression/cprover/basic/basic4.desc index 1aaf8f0de0e..d611b749ef1 100644 --- a/regression/cprover/basic/basic4.desc +++ b/regression/cprover/basic/basic4.desc @@ -3,9 +3,9 @@ basic4.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=2\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- diff --git a/regression/cprover/basic/basic5.desc b/regression/cprover/basic/basic5.desc index d0f62ff8464..88c85d3d101 100644 --- a/regression/cprover/basic/basic5.desc +++ b/regression/cprover/basic/basic5.desc @@ -3,12 +3,12 @@ basic5.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$ -^\(\d+\) S25 = S24$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$ +^\(\d+\) S24 = S23$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/basic6.desc b/regression/cprover/basic/basic6.desc index 7bbc6dd7c54..0dc2126c9d3 100644 --- a/regression/cprover/basic/basic6.desc +++ b/regression/cprover/basic/basic6.desc @@ -3,11 +3,11 @@ basic6.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$ +^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ +^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ ^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ ^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ ^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$ +^\(27\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/nondet1.desc b/regression/cprover/basic/nondet1.desc index f902da15fbd..014d21b7ca5 100644 --- a/regression/cprover/basic/nondet1.desc +++ b/regression/cprover/basic/nondet1.desc @@ -3,13 +3,13 @@ nondet1.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$ -^\(\d+\) S23 = S22$ -^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$ -^\(\d+\) S25 = S24$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=nondet::S21-0\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$ +^\(\d+\) S22 = S21$ +^\(\d+\) ∀ ς : state, nondet::S23-0 : signedbv\[32\] \. S22\(ς\) ⇒ S23\(ς\[❝main::1::y❞:=nondet::S23-0\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$ +^\(\d+\) S24 = S23$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=0\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/branching/branching1.desc b/regression/cprover/branching/branching1.desc index ff64a86eb44..79c277c2c95 100644 --- a/regression/cprover/branching/branching1.desc +++ b/regression/cprover/branching/branching1.desc @@ -3,20 +3,20 @@ branching1.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S21T\(\ς\)$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ +^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S20T\(\ς\)$ +^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S20\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(0 ≠ 0\)$ ^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$ ^\(\d+\) S23 = S22$ -^\(\d+\) S24 = S23$ -^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$ -^\(\d+\) S25 = S21T$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$ -^\(\d+\) S26 = S25$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$ -^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$ -^\(\d+\) S27 = S27in$ +^\(\d+\) ∀ ς : state \. S20T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$ +^\(\d+\) S24 = S20T$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(0 ≠ 0\)$ +^\(\d+\) S25 = S24$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S26in\(ς\)$ +^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$ +^\(\d+\) S26 = S26in$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ ^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$ diff --git a/regression/cprover/branching/branching2.desc b/regression/cprover/branching/branching2.desc index 53d98c6674a..d2418899a49 100644 --- a/regression/cprover/branching/branching2.desc +++ b/regression/cprover/branching/branching2.desc @@ -3,14 +3,14 @@ branching2.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$ -^\(\d+\) S24 = S23$ -^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$ -^\(\d+\) S26 = S26in$ +^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S21T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S21\(ς\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::b❞:=1\]\)$ +^\(\d+\) S23 = S22$ +^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S24\(ς\[❝main::1::b❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S25in\(ς\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25in\(ς\)$ +^\(\d+\) S25 = S25in$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/float/basic-float1.desc b/regression/cprover/float/basic-float1.desc index f166c3d1380..d71af0025f4 100644 --- a/regression/cprover/float/basic-float1.desc +++ b/regression/cprover/float/basic-float1.desc @@ -3,7 +3,7 @@ basic-float1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$ ^\[main\.assertion\.1\] line \d+ addition: SUCCESS$ -- diff --git a/regression/cprover/function_calls/call_no_body1.desc b/regression/cprover/function_calls/call_no_body1.desc index fe1c8685695..439eb9957e2 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::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S28\.2-0\]\)$ -^\(\d+\) ∀ ς : state \. S28\.2\(ς\) ⇒ S28\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ +^\(\d+\) ∀ ς : state, nondet::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S27\.2-0\]\)$ +^\(\d+\) ∀ ς : state \. S27\.2\(ς\) ⇒ S27\.3\(ς\[❝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 05093778b48..fe5f5d80a31 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::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S28\.2-0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S27\.2-0\]\)$ -- diff --git a/regression/cprover/loops/do_while1.desc b/regression/cprover/loops/do_while1.desc index fa38eb3a586..2fdf8c4d48f 100644 --- a/regression/cprover/loops/do_while1.desc +++ b/regression/cprover/loops/do_while1.desc @@ -3,12 +3,12 @@ do_while1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S23T\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. S22in\(ς\) ⇒ S22\(ς\[❝x❞:=20\]\)$ -^\(\d+\) ∀ ς : state . \(S22\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S23T\(ς\)$ -^\(\d+\) ∀ ς : state . \(S22\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S23\(ς\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. S21in\(ς\) ⇒ S21\(ς\[❝x❞:=20\]\)$ +^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S22T\(ς\)$ +^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S22\(ς\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/loops/for1.desc b/regression/cprover/loops/for1.desc index c9e443cfc46..769bca6223b 100644 --- a/regression/cprover/loops/for1.desc +++ b/regression/cprover/loops/for1.desc @@ -3,14 +3,14 @@ for1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S22\(ς\)$ -^\(\d+\) S23 = S22$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$ -^\(\d+\) S25 = S24$ -^\(\d+\) S26 = S22T$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S21T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S21\(ς\)$ +^\(\d+\) S22 = S21$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$ +^\(\d+\) S24 = S23$ +^\(\d+\) S25 = S21T$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/loops/for2.desc b/regression/cprover/loops/for2.desc index 8b0f17e74ff..d1c005203ba 100644 --- a/regression/cprover/loops/for2.desc +++ b/regression/cprover/loops/for2.desc @@ -3,12 +3,12 @@ for2.c --text --solve --unwind 10 --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S22\(ς\)$ -^\(\d+\) S23 = S22$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S21T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S21\(ς\)$ +^\(\d+\) S22 = S21$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- -- diff --git a/regression/cprover/loops/while-break1.desc b/regression/cprover/loops/while-break1.desc index 6b8f4c5c8de..cc39b1978d8 100644 --- a/regression/cprover/loops/while-break1.desc +++ b/regression/cprover/loops/while-break1.desc @@ -3,15 +3,15 @@ while-break1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S28\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ 1 ≠ 0\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S23T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S23\(ς\)$ -^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S29in\(ς\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S29in\(ς\)$ -^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S29in\(ς\)$ +^\(\d+\) ∀ ς : state \. S27\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S21T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ 1 ≠ 0\) ⇒ S21\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S22T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S22\(ς\)$ +^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S28in\(ς\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S28in\(ς\)$ +^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S28in\(ς\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/pointers/malloc1.desc b/regression/cprover/pointers/malloc1.desc index 775ddcbbaf9..c8481f22495 100644 --- a/regression/cprover/pointers/malloc1.desc +++ b/regression/cprover/pointers/malloc1.desc @@ -3,6 +3,6 @@ malloc1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers0.desc b/regression/cprover/pointers/pointers0.desc index 9ce4f642078..32715b07cd8 100644 --- a/regression/cprover/pointers/pointers0.desc +++ b/regression/cprover/pointers/pointers0.desc @@ -3,7 +3,7 @@ pointers0.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers1.desc b/regression/cprover/pointers/pointers1.desc index 46ccbfe4633..94dffb46dbb 100644 --- a/regression/cprover/pointers/pointers1.desc +++ b/regression/cprover/pointers/pointers1.desc @@ -3,9 +3,9 @@ pointers1.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers2.desc b/regression/cprover/pointers/pointers2.desc index b39c93b79b2..b753f6882e0 100644 --- a/regression/cprover/pointers/pointers2.desc +++ b/regression/cprover/pointers/pointers2.desc @@ -3,12 +3,12 @@ pointers2.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$ -^\(\d+\) S25 = S24$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝p❞\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$ +^\(\d+\) S24 = S23$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ ^\[main\.assertion\.1] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/pointers/pointers3.desc b/regression/cprover/pointers/pointers3.desc index b8b51405977..e79cbc8ce9a 100644 --- a/regression/cprover/pointers/pointers3.desc +++ b/regression/cprover/pointers/pointers3.desc @@ -3,7 +3,7 @@ pointers3.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S20\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers4.desc b/regression/cprover/pointers/pointers4.desc index 1569fe88769..4dbe138bc16 100644 --- a/regression/cprover/pointers/pointers4.desc +++ b/regression/cprover/pointers/pointers4.desc @@ -3,9 +3,9 @@ pointers4.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- diff --git a/regression/cprover/pointers/pointers5.desc b/regression/cprover/pointers/pointers5.desc index 453b44b3ea6..918b0cbaa9b 100644 --- a/regression/cprover/pointers/pointers5.desc +++ b/regression/cprover/pointers/pointers5.desc @@ -3,7 +3,7 @@ pointers5.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S23\(ς\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$ +^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S22\(ς\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers6.desc b/regression/cprover/pointers/pointers6.desc index 35c1dff9a5b..bc611d02779 100644 --- a/regression/cprover/pointers/pointers6.desc +++ b/regression/cprover/pointers/pointers6.desc @@ -3,9 +3,9 @@ pointers6.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=10\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::q❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers7.desc b/regression/cprover/pointers/pointers7.desc index 6f18eb76bfb..fc30acba3ee 100644 --- a/regression/cprover/pointers/pointers7.desc +++ b/regression/cprover/pointers/pointers7.desc @@ -3,14 +3,14 @@ pointers7.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$ -^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝p❞:=NULL\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)$ +^\(\d+\) S20 = S19$ ^\(\d+\) S21 = S20$ -^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=❝y❞\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝y❞\]\)$ +^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ ^\[main\.assertion\.1\] line \d property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers8.desc b/regression/cprover/pointers/pointers8.desc index c56a19d3e73..b17c7554b7b 100644 --- a/regression/cprover/pointers/pointers8.desc +++ b/regression/cprover/pointers/pointers8.desc @@ -3,8 +3,8 @@ pointers8.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[ς\(❝main::1::p❞\):=123\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝main::1::p❞\):=123\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers9.desc b/regression/cprover/pointers/pointers9.desc index aa097d00389..b511fd5605b 100644 --- a/regression/cprover/pointers/pointers9.desc +++ b/regression/cprover/pointers/pointers9.desc @@ -3,9 +3,9 @@ pointers9.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S23T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S23\(ς\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S22T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S22\(ς\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/struct_pointer1.desc b/regression/cprover/pointers/struct_pointer1.desc index 8582daf8386..22c20762c69 100644 --- a/regression/cprover/pointers/struct_pointer1.desc +++ b/regression/cprover/pointers/struct_pointer1.desc @@ -3,8 +3,8 @@ struct_pointer1.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/struct_pointer2.desc b/regression/cprover/pointers/struct_pointer2.desc index 620e0f42d4a..fc42c08c689 100644 --- a/regression/cprover/pointers/struct_pointer2.desc +++ b/regression/cprover/pointers/struct_pointer2.desc @@ -3,8 +3,8 @@ struct_pointer2.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/safety/use_after_free1.desc b/regression/cprover/safety/use_after_free1.desc index 55f42a70080..f77addc0862 100644 --- a/regression/cprover/safety/use_after_free1.desc +++ b/regression/cprover/safety/use_after_free1.desc @@ -3,6 +3,6 @@ use_after_free1.c --text --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state . S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$ -^\(\d+\) ∀ ς : state . S25\(ς\) ⇒ S26\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ +^\(\d+\) ∀ ς : state . S20\(ς\) ⇒ S21\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$ +^\(\d+\) ∀ ς : state . S24\(ς\) ⇒ S25\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ -- diff --git a/regression/cprover/structs/nondet_struct1.desc b/regression/cprover/structs/nondet_struct1.desc index e7c54f6c58e..c4642ab78fb 100644 --- a/regression/cprover/structs/nondet_struct1.desc +++ b/regression/cprover/structs/nondet_struct1.desc @@ -3,5 +3,5 @@ nondet_struct1.c --text --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\], nondet::S21-1 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝s❞\.❝x❞:=nondet::S21-0\]\[❝s❞\.❝y❞:=nondet::S21-1\]\)$ +^\(\d+\) ∀ ς : state, nondet::S20-0 : signedbv\[32\], nondet::S20-1 : signedbv\[32\] \. S19\(ς\) ⇒ S20\(ς\[❝s❞\.❝x❞:=nondet::S20-0\]\[❝s❞\.❝y❞:=nondet::S20-1\]\)$ -- diff --git a/regression/cprover/structs/struct1.desc b/regression/cprover/structs/struct1.desc index 0c58df9e6a3..15017b2a910 100644 --- a/regression/cprover/structs/struct1.desc +++ b/regression/cprover/structs/struct1.desc @@ -3,7 +3,7 @@ struct1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝s❞.❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/structs/struct2.desc b/regression/cprover/structs/struct2.desc index a260597c06e..c010b91a8f5 100644 --- a/regression/cprover/structs/struct2.desc +++ b/regression/cprover/structs/struct2.desc @@ -3,10 +3,10 @@ struct2.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝s❞.❝y❞:=2\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝s❞.❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝y❞:=2\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$ -- diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc index 8eb05ff4f8d..c51f496f971 100644 --- a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 47aea19e28b..f72aa419355 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc index 89bcfe85984..7e00b3bede2 100644 --- a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 0cc5f61bb73..db6a72b0380 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc index 89bcfe85984..7e00b3bede2 100644 --- a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 0cc5f61bb73..db6a72b0380 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc index 89bcfe85984..7e00b3bede2 100644 --- a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 0cc5f61bb73..db6a72b0380 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc index d4c16c2278f..876b363016a 100644 --- a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 22058dcb77e..7e53c699b10 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index 5ddf203f9b3..cc0c1eaedc1 100644 --- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc index 8d26811ac53..d475366b1a4 100644 --- a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index e63b5b8a837..99a72695b39 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc index bcc8b541c93..2ea9b96b541 100644 --- a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 79fcdf4a79b..d479d74b8c4 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ -- ^warning: ignoring 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 2a8b2b0aa11..0674acf000b 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 @ \[25\] +globalX .* 0 @ \[24\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[28\] +globalX .* TOP @ \[27\] -- 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 dd242a3a3e6..c64cd8df348 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 @ \[25\] +globalX .* 0 @ \[24\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[28\] +globalX .* TOP @ \[27\] -- 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 8de3a82a5ef..433cf42e8fb 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 @ \[25\] +globalX .* 0 @ \[24\] globalX .* 1 @ \[0\] globalX .* TOP @ \[0, 3\] -- 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 c8daf2ef143..c621a1baa37 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 @ \[25\] +globalX .* 0 @ \[24\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -- 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 92cff667e02..1bac1fddfc1 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -12,26 +12,25 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] __CPROVER_memory_leak \(\) -> TOP @ \[9\] __CPROVER_new_object \(\) -> TOP @ \[10\] __CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_arrays::1::bool_ \(\) -> TOP @ \[20\] -do_arrays::1::bool_1 \(\) -> TOP @ \[21\] -do_arrays::1::bool_2 \(\) -> TOP @ \[22\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\} @ \[24\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\[1\] = 20 @ \[25\]\n\} @ \[25\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 20 @ \[25\]\n\} @ \[26\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 40 @ \[27\]\n\} @ \[27\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 30 @ \[28\]\n\} @ \[28\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[28\]\n\} @ \[29\] -do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[30\]\n\[1\] = 30 @ \[28\]\n\} @ \[30\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 30 @ \[28\]\n\} @ \[31\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 10 @ \[32\]\n\} @ \[32\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\, 36\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\, 36\] -do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[38]\n\[1\] = 10 @ \[32\]\n\} @ \[38\] -do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[40]\n\[1\] = 10 @ \[32\]\n\} @ \[40\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42]\n\[1\] = 10 @ \[32\]\n\} @ \[40\, 42\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42\, 45]\n\[1\] = 10 @ \[47\]\n\} @ \[47\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[48]\n\[1\] = 10 @ \[47\]\n\} @ \[48\] +__CPROVER_rounding_mode \(\) -> 0 @ \[13\] +__CPROVER_thread_id \(\) -> 0ul @ \[14\] +__CPROVER_threads_exited \(\) -> TOP @ \[17\] +do_arrays::1::bool_ \(\) -> TOP @ \[19\] +do_arrays::1::bool_1 \(\) -> TOP @ \[20\] +do_arrays::1::bool_2 \(\) -> TOP @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\} @ \[23\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\[1\] = 20 @ \[24\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 20 @ \[24\]\n\} @ \[25\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 40 @ \[26\]\n\} @ \[26\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[27\]\n\} @ \[27\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[27\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[29\]\n\[1\] = 30 @ \[27\]\n\} @ \[29\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 30 @ \[27\]\n\} @ \[30\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 10 @ \[31\]\n\} @ \[31\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\, 35\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\, 35\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[37]\n\[1\] = 10 @ \[31\]\n\} @ \[37\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[39]\n\[1\] = 10 @ \[31\]\n\} @ \[39\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41]\n\[1\] = 10 @ \[31\]\n\} @ \[39\, 41\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41\, 44]\n\[1\] = 10 @ \[46\]\n\} @ \[46\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[47]\n\[1\] = 10 @ \[46\]\n\} @ \[47\] 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 bf14f6154f4..c0fd0b798de 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -12,25 +12,24 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] __CPROVER_memory_leak \(\) -> TOP @ \[9\] __CPROVER_new_object \(\) -> TOP @ \[10\] __CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_pointers::1::bool_ \(\) -> TOP @ \[20\] -do_pointers::1::bool_1 \(\) -> TOP @ \[21\] -do_pointers::1::bool_2 \(\) -> TOP @ \[22\] -do_pointers::1::x \(\) -> TOP @ \[23\] -do_pointers::1::x \(\) -> 10 @ \[24\] -do_pointers::1::x_p \(\) -> TOP @ \[25\] -do_pointers::1::y \(\) -> TOP @ \[26\] -do_pointers::1::y \(\) -> 20 @ \[27\] -do_pointers::1::y_p \(\) -> TOP @ \[28\] -do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[29\] -do_pointers::1::x \(\) -> 30 @ \[30\] -do_pointers::1::x \(\) -> 40 @ \[31\] -do_pointers::1::x \(\) -> TOP @ \[32\] -do_pointers::1::x \(\) -> 50 @ \[33\] -do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\] -do_pointers::1::x \(\) -> 60 @ \[35\] -do_pointers::1::j \(\) -> TOP @ \[36\] -do_pointers::1::j \(\) -> 60 @ \[37\] +__CPROVER_rounding_mode \(\) -> 0 @ \[13\] +__CPROVER_thread_id \(\) -> 0ul @ \[14\] +__CPROVER_threads_exited \(\) -> TOP @ \[17\] +do_pointers::1::bool_ \(\) -> TOP @ \[19\] +do_pointers::1::bool_1 \(\) -> TOP @ \[20\] +do_pointers::1::bool_2 \(\) -> TOP @ \[21\] +do_pointers::1::x \(\) -> TOP @ \[22\] +do_pointers::1::x \(\) -> 10 @ \[23\] +do_pointers::1::x_p \(\) -> TOP @ \[24\] +do_pointers::1::y \(\) -> TOP @ \[25\] +do_pointers::1::y \(\) -> 20 @ \[26\] +do_pointers::1::y_p \(\) -> TOP @ \[27\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\] +do_pointers::1::x \(\) -> 30 @ \[29\] +do_pointers::1::x \(\) -> 40 @ \[30\] +do_pointers::1::x \(\) -> TOP @ \[31\] +do_pointers::1::x \(\) -> 50 @ \[32\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[33\] +do_pointers::1::x \(\) -> 60 @ \[34\] +do_pointers::1::j \(\) -> TOP @ \[35\] +do_pointers::1::j \(\) -> 60 @ \[36\] 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 9b63fdf295e..59091198e9b 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -12,31 +12,30 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] __CPROVER_memory_leak \(\) -> TOP @ \[9\] __CPROVER_new_object \(\) -> TOP @ \[10\] __CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_structs::1::bool_ \(\) -> TOP @ \[20\] -do_structs::1::bool_1 \(\) -> TOP @ \[21\] -do_structs::1::bool_2 \(\) -> TOP @ \[22\] -do_structs::1::st \(\) -> \{\} @ \[23\] -do_structs::1::st \(\) -> \{.x=10 @ \[24\]\} @ \[24\] -do_structs::1::st \(\) -> \{.x=10 @ \[24\]\, .y=20 @ \[25\]\} @ \[25\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=20 @ \[25\]\} @ \[26\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=40 @ \[27\]\} @ \[27\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=30 @ \[28\]\} @ \[28\] -do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[28\]\} @ \[29\] -do_structs::1::st \(\) -> \{.x=5 @ \[30\]\, .y=30 @ \[28\]\} @ \[30\] -do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=30 @ \[28\]\} @ \[31\] -do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=10 @ \[32\]\} @ \[32\] -do_structs::1::st \(\) -> \{.x=20 @ \[34\]\, .y=10 @ \[32\]\} @ \[34\] -do_structs::1::st \(\) -> \{.x=20 @ \[34\, 36\]\, .y=10 @ \[32\]\} @ \[34\, 36\] -do_structs::1::st \(\) -> \{.x=0 @ \[38\]\, .y=10 @ \[32\]\} @ \[38\] -do_structs::1::st \(\) -> \{.x=3 @ \[40\]\, .y=10 @ \[32\]\} @ \[40\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\]\, .y=10 @ \[32\]\} @ \[40\, 42\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[32\]\} @ \[40\, 42\, 45\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[47\]\} @ \[47\] -do_structs::1::st \(\) -> \{.x=20 @ \[48\]\, .y=10 @ \[47\]\} @ \[48\] -do_structs::1::new_age \(\) -> \{\} @ \[49\] -do_structs::1::new_age \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[50\]\} @ \[50\] +__CPROVER_rounding_mode \(\) -> 0 @ \[13\] +__CPROVER_thread_id \(\) -> 0ul @ \[14\] +__CPROVER_threads_exited \(\) -> TOP @ \[17\] +do_structs::1::bool_ \(\) -> TOP @ \[19\] +do_structs::1::bool_1 \(\) -> TOP @ \[20\] +do_structs::1::bool_2 \(\) -> TOP @ \[21\] +do_structs::1::st \(\) -> \{\} @ \[22\] +do_structs::1::st \(\) -> \{.x=10 @ \[23\]\} @ \[23\] +do_structs::1::st \(\) -> \{.x=10 @ \[23\]\, .y=20 @ \[24\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=20 @ \[24\]\} @ \[25\] +do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=40 @ \[26\]\} @ \[26\] +do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=30 @ \[27\]\} @ \[27\] +do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[27\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=5 @ \[29\]\, .y=30 @ \[27\]\} @ \[29\] +do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=30 @ \[27\]\} @ \[30\] +do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=10 @ \[31\]\} @ \[31\] +do_structs::1::st \(\) -> \{.x=20 @ \[33\]\, .y=10 @ \[31\]\} @ \[33\] +do_structs::1::st \(\) -> \{.x=20 @ \[33\, 35\]\, .y=10 @ \[31\]\} @ \[33\, 35\] +do_structs::1::st \(\) -> \{.x=0 @ \[37\]\, .y=10 @ \[31\]\} @ \[37\] +do_structs::1::st \(\) -> \{.x=3 @ \[39\]\, .y=10 @ \[31\]\} @ \[39\] +do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\]\, .y=10 @ \[31\]\} @ \[39\, 41\] +do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[31\]\} @ \[39\, 41\, 44\] +do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[46\]\} @ \[46\] +do_structs::1::st \(\) -> \{.x=20 @ \[47\]\, .y=10 @ \[46\]\} @ \[47\] +do_structs::1::new_age \(\) -> \{\} @ \[48\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[49\]\, .y=10 @ \[49\]\} @ \[49\] -- 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 37eb13074fc..939236409ca 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -11,35 +11,34 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] __CPROVER_memory_leak \(\) -> TOP @ \[9\] __CPROVER_new_object \(\) -> TOP @ \[10\] __CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -global_x \(\) -> 0 @ \[19\] -do_variables::1::bool_ \(\) -> TOP @ \[21\] -do_variables::1::bool_1 \(\) -> TOP @ \[22\] -do_variables::1::bool_2 \(\) -> TOP @ \[23\] -global_x \(\) -> 5 @ \[24\] -do_variables::1::x \(\) -> TOP @ \[25\] -do_variables::1::x \(\) -> 10 @ \[26\] -do_variables::1::y \(\) -> TOP @ \[27\] -do_variables::1::y \(\) -> 20 @ \[28\] -do_variables::1::x \(\) -> 30 @ \[29\] -do_variables::1::y \(\) -> 40 @ \[30\] -do_variables::1::y \(\) -> 30 @ \[31\] -do_variables::1::x \(\) -> 30 @ \[32\] -do_variables::1::x \(\) -> 5 @ \[33\] -do_variables::1::x \(\) -> 15 @ \[34\] -do_variables::1::y \(\) -> 10 @ \[35\] -do_variables::1::x \(\) -> 20 @ \[37\] -do_variables::1::x \(\) -> 20 @ \[37\, 39\] -do_variables::1::x \(\) -> 50 @ \[41\] -do_variables::1::x \(\) -> 20 @ \[43\] -do_variables::1::x \(\) -> TOP @ \[43\, 45\] -do_variables::1::x \(\) -> 0 @ \[47\] -do_variables::1::x \(\) -> 3 @ \[49\] -do_variables::1::x \(\) -> TOP @ \[49\, 51\] -do_variables::1::x \(\) -> TOP @ \[49\, 51\, 54\] -do_variables::1::y \(\) -> 10 @ \[56\] -do_variables::1::x \(\) -> 20 @ \[57\] +__CPROVER_rounding_mode \(\) -> 0 @ \[13\] +__CPROVER_thread_id \(\) -> 0ul @ \[14\] +__CPROVER_threads_exited \(\) -> TOP @ \[17\] +global_x \(\) -> 0 @ \[18\] +do_variables::1::bool_ \(\) -> TOP @ \[20\] +do_variables::1::bool_1 \(\) -> TOP @ \[21\] +do_variables::1::bool_2 \(\) -> TOP @ \[22\] +global_x \(\) -> 5 @ \[23\] +do_variables::1::x \(\) -> TOP @ \[24\] +do_variables::1::x \(\) -> 10 @ \[25\] +do_variables::1::y \(\) -> TOP @ \[26\] +do_variables::1::y \(\) -> 20 @ \[27\] +do_variables::1::x \(\) -> 30 @ \[28\] +do_variables::1::y \(\) -> 40 @ \[29\] +do_variables::1::y \(\) -> 30 @ \[30\] +do_variables::1::x \(\) -> 30 @ \[31\] +do_variables::1::x \(\) -> 5 @ \[32\] +do_variables::1::x \(\) -> 15 @ \[33\] +do_variables::1::y \(\) -> 10 @ \[34\] +do_variables::1::x \(\) -> 20 @ \[36\] +do_variables::1::x \(\) -> 20 @ \[36\, 38\] +do_variables::1::x \(\) -> 50 @ \[40\] +do_variables::1::x \(\) -> 20 @ \[42\] +do_variables::1::x \(\) -> TOP @ \[42\, 44\] +do_variables::1::x \(\) -> 0 @ \[46\] +do_variables::1::x \(\) -> 3 @ \[48\] +do_variables::1::x \(\) -> TOP @ \[48\, 50\] +do_variables::1::x \(\) -> TOP @ \[48\, 50\, 53\] +do_variables::1::y \(\) -> 10 @ \[55\] +do_variables::1::x \(\) -> 20 @ \[56\] -- 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 e070c053f6f..186103d0a09 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, 52\]\[Data dependencies: 52, 2\]\[Data dominators: \], .b=.* @ \[5, 52\]\[Data dependencies: 52, 5\]\[Data dominators: \]\} @ \[2, 5, 52\]\[Data dependencies: 52, 5, 2\]\[Data dominators: 52\] -ar \(\) -> \{\[0\] = TOP @ \[11\, 46\]\[Data dependencies: 46\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 46\]\[Data dependencies: 46\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 46\]\[Data dependencies: 46\, 14\, 11\]\[Data dominators: 46\] -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: 47\] +st \(\) -> \{.a=.* @ \[2, 51\]\[Data dependencies: 51, 2\]\[Data dominators: \], .b=.* @ \[5, 51\]\[Data dependencies: 51, 5\]\[Data dominators: \]\} @ \[2, 5, 51\]\[Data dependencies: 51, 5, 2\]\[Data dominators: 51\] +ar \(\) -> \{\[0\] = TOP @ \[11\, 45\]\[Data dependencies: 45\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 45\]\[Data dependencies: 45\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 45\]\[Data dependencies: 45\, 14\, 11\]\[Data dominators: 45\] +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: 46\] -- ^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 1bd4f4ec3b5..d1be3190907 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 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 58 \[st.a\]$ -^Data dependencies: 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 57 \[st.a\]$ +^Data dependencies: 57 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 57 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 57 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\]$ +^Data dependencies: 51 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 51 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[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\], 58 \[st.a\], 62 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 57 \[st.a\], 61 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 57 \[st.b\], 64 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\], 61 \[st.a\], 64 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\], 72 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)0\]\], 75 \[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 a87e2b7a739..55d232cac2f 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 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 58 \[st.a\]$ -^Data dependencies: 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 57 \[st.a\]$ +^Data dependencies: 57 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 57 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 57 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\]$ +^Data dependencies: 51 \[ar\[\([^)]*\)0\]\]$ ^Data dependencies: 6 \[out1\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 51 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[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\], 58 \[st.a\], 62 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 57 \[st.a\], 61 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 57 \[st.b\], 64 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\], 61 \[st.a\], 64 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\], 72 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index fc1a4eff163..23d06c02fb3 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: 34 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] +\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 33 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] -- diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index d5f4911e4f4..a69af2a2679 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -209,11 +209,6 @@ void ansi_c_internal_additions(std::string &code) " short next_avail;\n" " short next_unread;\n" "};\n" - "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes[" - CPROVER_PREFIX "constant_infinity_uint];\n" - // offset to make sure we don't collide with other fds - "extern const int " CPROVER_PREFIX "pipe_offset;\n" - "unsigned " CPROVER_PREFIX "pipe_count=0;\n" "\n" // This function needs to be declared, or otherwise can't be called // by the entry-point construction. diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 16b17990ea8..7b2e8f27a7d 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -18,6 +18,8 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t; // NOLINTNEXTLINE(readability/identifiers) typedef signed long long __CPROVER_ssize_t; +#define __CPROVER_constant_infinity_uint 1 + void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); void __CPROVER_deallocate(void *); extern const void *__CPROVER_deallocated; diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 333cfc2a045..7fde194e53e 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -45,10 +45,10 @@ int unlink(const char *s) #define __CPROVER_ERRNO_H_INCLUDED #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; -extern unsigned __CPROVER_pipe_count; +unsigned __CPROVER_pipe_count = 0; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); @@ -97,7 +97,7 @@ __CPROVER_HIDE:; /* FUNCTION: close */ -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -151,7 +151,7 @@ int _close(int fildes) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -229,7 +229,7 @@ ret_type _write(int fildes, const void *buf, size_type nbyte) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index c1365387c83..993ddc9735b 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -119,11 +119,6 @@ void cpp_internal_additions(std::ostream &out) << " short next_avail;\n" << " short next_unread;\n" << "};\n"; - out << "extern struct " CPROVER_PREFIX "pipet " - << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n'; - // offset to make sure we don't collide with other fds - out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n'; - out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n'; // This function needs to be declared, or otherwise can't be called // by the entry-point construction. From da4c6ec4634949f7a9c93896b7eca390a4beeac9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 29 Sep 2022 09:31:05 +0000 Subject: [PATCH 5/6] C/C++ library: move free/delete-only definitions to library With the support of building initialisers while adding the library we can move library-only symbols to the library. This avoids polluting the initialisation function for all cases that don't actually use memory (de-)allocation library functions. --- regression/cbmc-library/alloca-02/main.c | 5 ++ regression/cbmc-library/alloca-02/test.desc | 2 +- .../cbmc/xml-escaping/debug_output.desc | 1 - regression/cprover/arrays/array1.desc | 10 +-- regression/cprover/arrays/array2.desc | 6 +- regression/cprover/basic/assume1.desc | 6 +- regression/cprover/basic/basic1.desc | 6 +- regression/cprover/basic/basic2.desc | 10 +-- regression/cprover/basic/basic3.desc | 10 +-- regression/cprover/basic/basic4.desc | 8 +-- regression/cprover/basic/basic5.desc | 12 ++-- regression/cprover/basic/basic6.desc | 10 +-- regression/cprover/basic/nondet1.desc | 14 ++-- regression/cprover/branching/branching1.desc | 24 +++---- regression/cprover/branching/branching2.desc | 16 ++--- regression/cprover/float/basic-float1.desc | 4 +- .../cprover/function_calls/call_no_body1.desc | 4 +- .../cprover/function_calls/call_no_body2.desc | 2 +- regression/cprover/loops/do_while1.desc | 12 ++-- regression/cprover/loops/for1.desc | 16 ++--- regression/cprover/loops/for2.desc | 12 ++-- regression/cprover/loops/while-break1.desc | 18 ++--- regression/cprover/pointers/malloc1.desc | 2 +- regression/cprover/pointers/pointers0.desc | 4 +- regression/cprover/pointers/pointers1.desc | 8 +-- regression/cprover/pointers/pointers2.desc | 12 ++-- regression/cprover/pointers/pointers3.desc | 4 +- regression/cprover/pointers/pointers4.desc | 8 +-- regression/cprover/pointers/pointers5.desc | 4 +- regression/cprover/pointers/pointers6.desc | 8 +-- regression/cprover/pointers/pointers7.desc | 18 ++--- regression/cprover/pointers/pointers8.desc | 6 +- regression/cprover/pointers/pointers9.desc | 8 +-- .../cprover/pointers/struct_pointer1.desc | 6 +- .../cprover/pointers/struct_pointer2.desc | 6 +- .../cprover/safety/use_after_free1.desc | 4 +- .../cprover/structs/nondet_struct1.desc | 2 +- regression/cprover/structs/struct1.desc | 4 +- regression/cprover/structs/struct2.desc | 8 +-- .../constant_propagation_01/test-vsd.desc | 4 +- .../constant_propagation_01/test.desc | 4 +- .../constant_propagation_02/test-vsd.desc | 4 +- .../constant_propagation_02/test.desc | 4 +- .../constant_propagation_03/test-vsd.desc | 4 +- .../constant_propagation_03/test.desc | 4 +- .../constant_propagation_04/test-vsd.desc | 4 +- .../constant_propagation_04/test.desc | 4 +- .../constant_propagation_07/test-vsd.desc | 4 +- .../constant_propagation_07/test.desc | 4 +- .../constant_propagation_08/test-vsd.desc | 4 +- .../constant_propagation_11/test-vsd.desc | 4 +- .../constant_propagation_11/test.desc | 4 +- .../constant_propagation_12/test-vsd.desc | 4 +- .../constant_propagation_12/test.desc | 4 +- .../test-liveness-show.desc | 4 +- .../test-liveness-three-way-show.desc | 4 +- .../test-write-location-show.desc | 2 +- .../test-write-location-three-way-show.desc | 2 +- .../test.desc | 54 +++++++-------- .../test.desc | 52 +++++++------- .../test.desc | 62 ++++++++--------- .../test.desc | 69 +++++++++---------- .../test.desc | 6 +- .../test.desc | 32 ++++----- .../test.desc | 32 ++++----- .../test.desc | 2 +- src/ansi-c/ansi_c_internal_additions.cpp | 3 - src/ansi-c/library/cprover.h | 2 - src/ansi-c/library/stdlib.c | 17 ++++- src/cpp/cpp_internal_additions.cpp | 4 -- src/cpp/library/cprover.h | 2 - src/cpp/library/new.c | 8 +++ 72 files changed, 371 insertions(+), 366 deletions(-) diff --git a/regression/cbmc-library/alloca-02/main.c b/regression/cbmc-library/alloca-02/main.c index 27dd244c4ad..d23244d6a88 100644 --- a/regression/cbmc-library/alloca-02/main.c +++ b/regression/cbmc-library/alloca-02/main.c @@ -4,9 +4,14 @@ void *alloca(size_t alloca_size); #endif +// intentionally type conflicting: the built-in library uses const void*; this +// is to check that object type updates are performed +extern const char *__CPROVER_alloca_object; + int *foo() { int *foo_ptr = alloca(sizeof(int)); + __CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail"); return foo_ptr; } diff --git a/regression/cbmc-library/alloca-02/test.desc b/regression/cbmc-library/alloca-02/test.desc index 3c2405a8436..273ea7118de 100644 --- a/regression/cbmc-library/alloca-02/test.desc +++ b/regression/cbmc-library/alloca-02/test.desc @@ -2,7 +2,7 @@ CORE main.c --pointer-check dereference failure: dead object in \*from_foo: FAILURE$ -^\*\* 1 of 6 failed +^\*\* 2 of 7 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/xml-escaping/debug_output.desc b/regression/cbmc/xml-escaping/debug_output.desc index ddfb415c818..af4f42c9fa8 100644 --- a/regression/cbmc/xml-escaping/debug_output.desc +++ b/regression/cbmc/xml-escaping/debug_output.desc @@ -4,7 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -⇔ false \¬main\:\:1\:\:x\!0\@1\#1 -- XML does not support escaping non-printable character diff --git a/regression/cprover/arrays/array1.desc b/regression/cprover/arrays/array1.desc index c191c70855d..392c8f6021c 100644 --- a/regression/cprover/arrays/array1.desc +++ b/regression/cprover/arrays/array1.desc @@ -3,11 +3,11 @@ array1.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$ ^\[main\.assertion\.3\] line \d+ property 3: REFUTED$ diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc index db7db1faf42..13549717763 100644 --- a/regression/cprover/arrays/array2.desc +++ b/regression/cprover/arrays/array2.desc @@ -3,9 +3,9 @@ array2.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S23\(ς\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$ +^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S20\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/assume1.desc b/regression/cprover/basic/assume1.desc index 7efdc15e8e2..c0e6961d14b 100644 --- a/regression/cprover/basic/assume1.desc +++ b/regression/cprover/basic/assume1.desc @@ -6,9 +6,9 @@ assume1.c ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$ ^ \(\d+\) S0 = SInitial$ ^ \(\d+\) S1 = S0$ -^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S20\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$ +^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S17\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/basic1.desc b/regression/cprover/basic/basic1.desc index 43759960f6d..63a7d8bb7a3 100644 --- a/regression/cprover/basic/basic1.desc +++ b/regression/cprover/basic/basic1.desc @@ -5,8 +5,8 @@ basic1.c ^SIGNAL=0$ ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$ ^ \(\d+\) S0 = SInitial$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic2.desc b/regression/cprover/basic/basic2.desc index 5ad0beb9fb1..125514e2e7b 100644 --- a/regression/cprover/basic/basic2.desc +++ b/regression/cprover/basic/basic2.desc @@ -3,11 +3,11 @@ basic2.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$ +^\(\d+\) S15 = S14$ +^\(\d+\) S16 = S15$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$ ^\(\d+\) S18 = S17$ -^\(\d+\) S19 = S18$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ -^\(\d+\) S21 = S20$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic3.desc b/regression/cprover/basic/basic3.desc index f49ba79b237..83ea8793963 100644 --- a/regression/cprover/basic/basic3.desc +++ b/regression/cprover/basic/basic3.desc @@ -3,10 +3,10 @@ basic3.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\) -\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝y❞:=0\]\) -\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\) -\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝y❞:=2\]\) -\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\) +\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\) +\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝y❞:=0\]\) +\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=1\]\) +\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=2\]\) +\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝x❞\) = 1\) ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/basic4.desc b/regression/cprover/basic/basic4.desc index d611b749ef1..0796e907534 100644 --- a/regression/cprover/basic/basic4.desc +++ b/regression/cprover/basic/basic4.desc @@ -3,9 +3,9 @@ basic4.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=2\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=2\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- diff --git a/regression/cprover/basic/basic5.desc b/regression/cprover/basic/basic5.desc index 88c85d3d101..f25d87f68d9 100644 --- a/regression/cprover/basic/basic5.desc +++ b/regression/cprover/basic/basic5.desc @@ -3,12 +3,12 @@ basic5.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$ -^\(\d+\) S24 = S23$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/basic/basic6.desc b/regression/cprover/basic/basic6.desc index 0dc2126c9d3..c5df6e233ac 100644 --- a/regression/cprover/basic/basic6.desc +++ b/regression/cprover/basic/basic6.desc @@ -3,11 +3,11 @@ basic6.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$ +^\(19\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$ +^\(20\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ +^\(21\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ +^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ ^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$ -^\(27\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$ +^\(24\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/basic/nondet1.desc b/regression/cprover/basic/nondet1.desc index 014d21b7ca5..060db73b9a0 100644 --- a/regression/cprover/basic/nondet1.desc +++ b/regression/cprover/basic/nondet1.desc @@ -3,13 +3,13 @@ nondet1.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=nondet::S21-0\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$ -^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state, nondet::S23-0 : signedbv\[32\] \. S22\(ς\) ⇒ S23\(ς\[❝main::1::y❞:=nondet::S23-0\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$ -^\(\d+\) S24 = S23$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S18-0 : signedbv\[32\] \. S17\(ς\) ⇒ S18\(ς\[❝main::1::x❞:=nondet::S18-0\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$ +^\(\d+\) S19 = S18$ +^\(\d+\) ∀ ς : state, nondet::S20-0 : signedbv\[32\] \. S19\(ς\) ⇒ S20\(ς\[❝main::1::y❞:=nondet::S20-0\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝return'❞:=0\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/branching/branching1.desc b/regression/cprover/branching/branching1.desc index 79c277c2c95..3263a8ddbbc 100644 --- a/regression/cprover/branching/branching1.desc +++ b/regression/cprover/branching/branching1.desc @@ -3,20 +3,20 @@ branching1.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S20T\(\ς\)$ -^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S20\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ -^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S17T\(\ς\)$ +^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S17\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$ +^\(\d+\) S18 = S17$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(0 ≠ 0\)$ +^\(\d+\) S19 = S18$ +^\(\d+\) S20 = S19$ +^\(\d+\) ∀ ς : state \. S17T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$ +^\(\d+\) S21 = S17T$ ^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(0 ≠ 0\)$ ^\(\d+\) S22 = S21$ -^\(\d+\) S23 = S22$ -^\(\d+\) ∀ ς : state \. S20T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$ -^\(\d+\) S24 = S20T$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(0 ≠ 0\)$ -^\(\d+\) S25 = S24$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S26in\(ς\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$ -^\(\d+\) S26 = S26in$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S23in\(ς\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23in\(ς\)$ +^\(\d+\) S23 = S23in$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ ^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$ diff --git a/regression/cprover/branching/branching2.desc b/regression/cprover/branching/branching2.desc index d2418899a49..4b61d61c406 100644 --- a/regression/cprover/branching/branching2.desc +++ b/regression/cprover/branching/branching2.desc @@ -3,14 +3,14 @@ branching2.c --text --solve --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S21T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::b❞:=1\]\)$ -^\(\d+\) S23 = S22$ -^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S24\(ς\[❝main::1::b❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S25in\(ς\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25in\(ς\)$ -^\(\d+\) S25 = S25in$ +^\(\d+\) ∀ ς : state \. \(S17\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S18T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S17\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S18\(ς\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::b❞:=1\]\)$ +^\(\d+\) S20 = S19$ +^\(\d+\) ∀ ς : state \. S18T\(ς\) ⇒ S21\(ς\[❝main::1::b❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S22in\(ς\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$ +^\(\d+\) S22 = S22in$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/float/basic-float1.desc b/regression/cprover/float/basic-float1.desc index d71af0025f4..2d1901348a6 100644 --- a/regression/cprover/float/basic-float1.desc +++ b/regression/cprover/float/basic-float1.desc @@ -3,7 +3,7 @@ basic-float1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$ ^\[main\.assertion\.1\] line \d+ addition: SUCCESS$ -- diff --git a/regression/cprover/function_calls/call_no_body1.desc b/regression/cprover/function_calls/call_no_body1.desc index 439eb9957e2..b6181fc37fe 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::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S27\.2-0\]\)$ -^\(\d+\) ∀ ς : state \. S27\.2\(ς\) ⇒ S27\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ +^\(\d+\) ∀ ς : state, nondet::S24\.2-0 : signedbv\[32\] \. S24\.1\(ς\) ⇒ S24\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S24\.2-0\]\)$ +^\(\d+\) ∀ ς : state \. S24\.2\(ς\) ⇒ S24\.3\(ς\[❝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 fe5f5d80a31..24dbf0d31ea 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::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S27\.2-0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S24\.2-0 : signedbv\[32\] \. S24\.1\(ς\) ⇒ S24\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S24\.2-0\]\)$ -- diff --git a/regression/cprover/loops/do_while1.desc b/regression/cprover/loops/do_while1.desc index 2fdf8c4d48f..b99025f9620 100644 --- a/regression/cprover/loops/do_while1.desc +++ b/regression/cprover/loops/do_while1.desc @@ -3,12 +3,12 @@ do_while1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. S21in\(ς\) ⇒ S21\(ς\[❝x❞:=20\]\)$ -^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S22\(ς\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S19T\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. S18in\(ς\) ⇒ S18\(ς\[❝x❞:=20\]\)$ +^\(\d+\) ∀ ς : state . \(S18\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S19T\(ς\)$ +^\(\d+\) ∀ ς : state . \(S18\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S19\(ς\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/loops/for1.desc b/regression/cprover/loops/for1.desc index 769bca6223b..026d2c889ce 100644 --- a/regression/cprover/loops/for1.desc +++ b/regression/cprover/loops/for1.desc @@ -3,14 +3,14 @@ for1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S21T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S21\(ς\)$ -^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$ -^\(\d+\) S24 = S23$ -^\(\d+\) S25 = S21T$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S18T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S18\(ς\)$ +^\(\d+\) S19 = S18$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) S22 = S18T$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/loops/for2.desc b/regression/cprover/loops/for2.desc index d1c005203ba..d36f5c93705 100644 --- a/regression/cprover/loops/for2.desc +++ b/regression/cprover/loops/for2.desc @@ -3,12 +3,12 @@ for2.c --text --solve --unwind 10 --inline ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S21T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S21\(ς\)$ -^\(\d+\) S22 = S21$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S18T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S18\(ς\)$ +^\(\d+\) S19 = S18$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- -- diff --git a/regression/cprover/loops/while-break1.desc b/regression/cprover/loops/while-break1.desc index cc39b1978d8..0e7f8f21655 100644 --- a/regression/cprover/loops/while-break1.desc +++ b/regression/cprover/loops/while-break1.desc @@ -3,15 +3,15 @@ while-break1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S27\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S21T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ 1 ≠ 0\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S28in\(ς\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S28in\(ς\)$ -^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S28in\(ς\)$ +^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S18T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ 1 ≠ 0\) ⇒ S18\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S19T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S19\(ς\)$ +^\(\d+\) ∀ ς : state \. S18T\(ς\) ⇒ S25in\(ς\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S25in\(ς\)$ +^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S25in\(ς\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- -- diff --git a/regression/cprover/pointers/malloc1.desc b/regression/cprover/pointers/malloc1.desc index c8481f22495..27cb747fb07 100644 --- a/regression/cprover/pointers/malloc1.desc +++ b/regression/cprover/pointers/malloc1.desc @@ -3,6 +3,6 @@ malloc1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers0.desc b/regression/cprover/pointers/pointers0.desc index 32715b07cd8..0cc60b14164 100644 --- a/regression/cprover/pointers/pointers0.desc +++ b/regression/cprover/pointers/pointers0.desc @@ -3,7 +3,7 @@ pointers0.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers1.desc b/regression/cprover/pointers/pointers1.desc index 94dffb46dbb..f5a14213727 100644 --- a/regression/cprover/pointers/pointers1.desc +++ b/regression/cprover/pointers/pointers1.desc @@ -3,9 +3,9 @@ pointers1.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers2.desc b/regression/cprover/pointers/pointers2.desc index b753f6882e0..055518c4e72 100644 --- a/regression/cprover/pointers/pointers2.desc +++ b/regression/cprover/pointers/pointers2.desc @@ -3,12 +3,12 @@ pointers2.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝p❞\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$ -^\(\d+\) S24 = S23$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝p❞\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$ +^\(\d+\) S21 = S20$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ ^\[main\.assertion\.1] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/pointers/pointers3.desc b/regression/cprover/pointers/pointers3.desc index e79cbc8ce9a..66387a137ce 100644 --- a/regression/cprover/pointers/pointers3.desc +++ b/regression/cprover/pointers/pointers3.desc @@ -3,7 +3,7 @@ pointers3.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S20\(ς\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S17\(ς\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers4.desc b/regression/cprover/pointers/pointers4.desc index 4dbe138bc16..311b80bca1c 100644 --- a/regression/cprover/pointers/pointers4.desc +++ b/regression/cprover/pointers/pointers4.desc @@ -3,9 +3,9 @@ pointers4.c --text --solve --inline --no-safety ^EXIT=10$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. \(S17\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S18\(ς\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$ -- diff --git a/regression/cprover/pointers/pointers5.desc b/regression/cprover/pointers/pointers5.desc index 918b0cbaa9b..8391ef375b0 100644 --- a/regression/cprover/pointers/pointers5.desc +++ b/regression/cprover/pointers/pointers5.desc @@ -3,7 +3,7 @@ pointers5.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$ +^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S19\(ς\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers6.desc b/regression/cprover/pointers/pointers6.desc index bc611d02779..75049e02f91 100644 --- a/regression/cprover/pointers/pointers6.desc +++ b/regression/cprover/pointers/pointers6.desc @@ -3,9 +3,9 @@ pointers6.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=10\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::q❞:=❝x❞\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::p❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝main::1::p❞\):=10\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::q❞:=❝x❞\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers7.desc b/regression/cprover/pointers/pointers7.desc index fc30acba3ee..dedf6a67c15 100644 --- a/regression/cprover/pointers/pointers7.desc +++ b/regression/cprover/pointers/pointers7.desc @@ -3,14 +3,14 @@ pointers7.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝p❞:=NULL\]\)$ -^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$ -^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)$ -^\(\d+\) S20 = S19$ -^\(\d+\) S21 = S20$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝y❞\]\)$ -^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$ -^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ +^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝p❞:=NULL\]\)$ +^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝x❞:=0\]\)$ +^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S16\(ς\[❝y❞:=0\]\)$ +^\(\d+\) S17 = S16$ +^\(\d+\) S18 = S17$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=10\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝p❞:=❝y❞\]\)$ +^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[ς\(❝p❞\):=20\]\)$ +^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$ ^\[main\.assertion\.1\] line \d property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers8.desc b/regression/cprover/pointers/pointers8.desc index b17c7554b7b..1b2c3f702dc 100644 --- a/regression/cprover/pointers/pointers8.desc +++ b/regression/cprover/pointers/pointers8.desc @@ -3,8 +3,8 @@ pointers8.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝main::1::p❞\):=123\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[ς\(❝main::1::p❞\):=123\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/pointers9.desc b/regression/cprover/pointers/pointers9.desc index b511fd5605b..634e8c8b013 100644 --- a/regression/cprover/pointers/pointers9.desc +++ b/regression/cprover/pointers/pointers9.desc @@ -3,9 +3,9 @@ pointers9.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S22T\(ς\)$ -^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S22\(ς\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::x❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S19T\(ς\)$ +^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S19\(ς\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/struct_pointer1.desc b/regression/cprover/pointers/struct_pointer1.desc index 22c20762c69..c15749d4535 100644 --- a/regression/cprover/pointers/struct_pointer1.desc +++ b/regression/cprover/pointers/struct_pointer1.desc @@ -3,8 +3,8 @@ struct_pointer1.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/pointers/struct_pointer2.desc b/regression/cprover/pointers/struct_pointer2.desc index fc42c08c689..586a8df01ca 100644 --- a/regression/cprover/pointers/struct_pointer2.desc +++ b/regression/cprover/pointers/struct_pointer2.desc @@ -3,8 +3,8 @@ struct_pointer2.c --text --solve --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/safety/use_after_free1.desc b/regression/cprover/safety/use_after_free1.desc index f77addc0862..2493545c121 100644 --- a/regression/cprover/safety/use_after_free1.desc +++ b/regression/cprover/safety/use_after_free1.desc @@ -3,6 +3,6 @@ use_after_free1.c --text --inline --no-safety ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state . S20\(ς\) ⇒ S21\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$ -^\(\d+\) ∀ ς : state . S24\(ς\) ⇒ S25\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ +^\(\d+\) ∀ ς : state . S17\(ς\) ⇒ S18\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$ +^\(\d+\) ∀ ς : state . S21\(ς\) ⇒ S22\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$ -- diff --git a/regression/cprover/structs/nondet_struct1.desc b/regression/cprover/structs/nondet_struct1.desc index c4642ab78fb..7ea9a774508 100644 --- a/regression/cprover/structs/nondet_struct1.desc +++ b/regression/cprover/structs/nondet_struct1.desc @@ -3,5 +3,5 @@ nondet_struct1.c --text --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S20-0 : signedbv\[32\], nondet::S20-1 : signedbv\[32\] \. S19\(ς\) ⇒ S20\(ς\[❝s❞\.❝x❞:=nondet::S20-0\]\[❝s❞\.❝y❞:=nondet::S20-1\]\)$ +^\(\d+\) ∀ ς : state, nondet::S17-0 : signedbv\[32\], nondet::S17-1 : signedbv\[32\] \. S16\(ς\) ⇒ S17\(ς\[❝s❞\.❝x❞:=nondet::S17-0\]\[❝s❞\.❝y❞:=nondet::S17-1\]\)$ -- diff --git a/regression/cprover/structs/struct1.desc b/regression/cprover/structs/struct1.desc index 15017b2a910..f2fc873bdb7 100644 --- a/regression/cprover/structs/struct1.desc +++ b/regression/cprover/structs/struct1.desc @@ -3,7 +3,7 @@ struct1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝s❞.❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝s❞.❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/cprover/structs/struct2.desc b/regression/cprover/structs/struct2.desc index c010b91a8f5..3e556d1b5e3 100644 --- a/regression/cprover/structs/struct2.desc +++ b/regression/cprover/structs/struct2.desc @@ -3,10 +3,10 @@ struct2.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝s❞.❝x❞:=1\]\)$ -^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝y❞:=2\]\)$ -^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ -^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$ +^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝s❞.❝x❞:=1\]\)$ +^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝s❞.❝y❞:=2\]\)$ +^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$ +^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$ -- diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc index c51f496f971..d498e0b409c 100644 --- a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index f72aa419355..a4a79f28ab1 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc index 7e00b3bede2..4d18142ff67 100644 --- a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index db6a72b0380..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc index 7e00b3bede2..4d18142ff67 100644 --- a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index db6a72b0380..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc index 7e00b3bede2..4d18142ff67 100644 --- a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index db6a72b0380..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc index 876b363016a..46bac02fac4 100644 --- a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 7e53c699b10..87b2c5112b0 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index cc0c1eaedc1..ce088476107 100644 --- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc index d475366b1a4..ba1ee57a8f7 100644 --- a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 99a72695b39..6653d122562 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc index 2ea9b96b541..2f4f1e9d2b4 100644 --- a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index d479d74b8c4..df5dd997788 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring 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 0674acf000b..f8ae2826abc 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 @ \[24\] +globalX .* 0 @ \[21\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[27\] +globalX .* TOP @ \[24\] -- 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 c64cd8df348..6a38f8f90a0 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 @ \[24\] +globalX .* 0 @ \[21\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[27\] +globalX .* TOP @ \[24\] -- 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 433cf42e8fb..d0ab8a1918d 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 @ \[24\] +globalX .* 0 @ \[21\] globalX .* 1 @ \[0\] globalX .* TOP @ \[0, 3\] -- 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 c621a1baa37..2f78ad7aaba 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 @ \[24\] +globalX .* 0 @ \[21\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -- 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 1bac1fddfc1..b698835de22 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -6,31 +6,29 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_rounding_mode \(\) -> 0 @ \[13\] -__CPROVER_thread_id \(\) -> 0ul @ \[14\] -__CPROVER_threads_exited \(\) -> TOP @ \[17\] -do_arrays::1::bool_ \(\) -> TOP @ \[19\] -do_arrays::1::bool_1 \(\) -> TOP @ \[20\] -do_arrays::1::bool_2 \(\) -> TOP @ \[21\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\} @ \[23\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\[1\] = 20 @ \[24\]\n\} @ \[24\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 20 @ \[24\]\n\} @ \[25\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 40 @ \[26\]\n\} @ \[26\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[27\]\n\} @ \[27\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[27\]\n\} @ \[28\] -do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[29\]\n\[1\] = 30 @ \[27\]\n\} @ \[29\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 30 @ \[27\]\n\} @ \[30\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 10 @ \[31\]\n\} @ \[31\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\, 35\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\, 35\] -do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[37]\n\[1\] = 10 @ \[31\]\n\} @ \[37\] -do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[39]\n\[1\] = 10 @ \[31\]\n\} @ \[39\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41]\n\[1\] = 10 @ \[31\]\n\} @ \[39\, 41\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41\, 44]\n\[1\] = 10 @ \[46\]\n\} @ \[46\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[47]\n\[1\] = 10 @ \[46\]\n\} @ \[47\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_next_thread_key \(\) -> 0ul @ \[9\] +__CPROVER_rounding_mode \(\) -> 0 @ \[10\] +__CPROVER_thread_id \(\) -> 0ul @ \[11\] +__CPROVER_threads_exited \(\) -> TOP @ \[14\] +do_arrays::1::bool_ \(\) -> TOP @ \[16\] +do_arrays::1::bool_1 \(\) -> TOP @ \[17\] +do_arrays::1::bool_2 \(\) -> TOP @ \[18\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\} @ \[20\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\[1\] = 20 @ \[21\]\n\} @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 20 @ \[21\]\n\} @ \[22\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 40 @ \[23\]\n\} @ \[23\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 30 @ \[24\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[24\]\n\} @ \[25\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[26\]\n\[1\] = 30 @ \[24\]\n\} @ \[26\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 30 @ \[24\]\n\} @ \[27\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 10 @ \[28\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\, 32\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\, 32\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[34]\n\[1\] = 10 @ \[28\]\n\} @ \[34\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[36]\n\[1\] = 10 @ \[28\]\n\} @ \[36\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38]\n\[1\] = 10 @ \[28\]\n\} @ \[36\, 38\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41]\n\[1\] = 10 @ \[43\]\n\} @ \[43\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[44]\n\[1\] = 10 @ \[43\]\n\} @ \[44\] 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 c0fd0b798de..b1d1e153d43 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -6,30 +6,28 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_rounding_mode \(\) -> 0 @ \[13\] -__CPROVER_thread_id \(\) -> 0ul @ \[14\] -__CPROVER_threads_exited \(\) -> TOP @ \[17\] -do_pointers::1::bool_ \(\) -> TOP @ \[19\] -do_pointers::1::bool_1 \(\) -> TOP @ \[20\] -do_pointers::1::bool_2 \(\) -> TOP @ \[21\] -do_pointers::1::x \(\) -> TOP @ \[22\] -do_pointers::1::x \(\) -> 10 @ \[23\] -do_pointers::1::x_p \(\) -> TOP @ \[24\] -do_pointers::1::y \(\) -> TOP @ \[25\] -do_pointers::1::y \(\) -> 20 @ \[26\] -do_pointers::1::y_p \(\) -> TOP @ \[27\] -do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\] -do_pointers::1::x \(\) -> 30 @ \[29\] -do_pointers::1::x \(\) -> 40 @ \[30\] -do_pointers::1::x \(\) -> TOP @ \[31\] -do_pointers::1::x \(\) -> 50 @ \[32\] -do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[33\] -do_pointers::1::x \(\) -> 60 @ \[34\] -do_pointers::1::j \(\) -> TOP @ \[35\] -do_pointers::1::j \(\) -> 60 @ \[36\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_next_thread_key \(\) -> 0ul @ \[9\] +__CPROVER_rounding_mode \(\) -> 0 @ \[10\] +__CPROVER_thread_id \(\) -> 0ul @ \[11\] +__CPROVER_threads_exited \(\) -> TOP @ \[14\] +do_pointers::1::bool_ \(\) -> TOP @ \[16\] +do_pointers::1::bool_1 \(\) -> TOP @ \[17\] +do_pointers::1::bool_2 \(\) -> TOP @ \[18\] +do_pointers::1::x \(\) -> TOP @ \[19\] +do_pointers::1::x \(\) -> 10 @ \[20\] +do_pointers::1::x_p \(\) -> TOP @ \[21\] +do_pointers::1::y \(\) -> TOP @ \[22\] +do_pointers::1::y \(\) -> 20 @ \[23\] +do_pointers::1::y_p \(\) -> TOP @ \[24\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[25\] +do_pointers::1::x \(\) -> 30 @ \[26\] +do_pointers::1::x \(\) -> 40 @ \[27\] +do_pointers::1::x \(\) -> TOP @ \[28\] +do_pointers::1::x \(\) -> 50 @ \[29\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\] +do_pointers::1::x \(\) -> 60 @ \[31\] +do_pointers::1::j \(\) -> TOP @ \[32\] +do_pointers::1::j \(\) -> 60 @ \[33\] 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 59091198e9b..0d84d60671a 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -6,36 +6,34 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_rounding_mode \(\) -> 0 @ \[13\] -__CPROVER_thread_id \(\) -> 0ul @ \[14\] -__CPROVER_threads_exited \(\) -> TOP @ \[17\] -do_structs::1::bool_ \(\) -> TOP @ \[19\] -do_structs::1::bool_1 \(\) -> TOP @ \[20\] -do_structs::1::bool_2 \(\) -> TOP @ \[21\] -do_structs::1::st \(\) -> \{\} @ \[22\] -do_structs::1::st \(\) -> \{.x=10 @ \[23\]\} @ \[23\] -do_structs::1::st \(\) -> \{.x=10 @ \[23\]\, .y=20 @ \[24\]\} @ \[24\] -do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=20 @ \[24\]\} @ \[25\] -do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=40 @ \[26\]\} @ \[26\] -do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=30 @ \[27\]\} @ \[27\] -do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[27\]\} @ \[28\] -do_structs::1::st \(\) -> \{.x=5 @ \[29\]\, .y=30 @ \[27\]\} @ \[29\] -do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=30 @ \[27\]\} @ \[30\] -do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=10 @ \[31\]\} @ \[31\] -do_structs::1::st \(\) -> \{.x=20 @ \[33\]\, .y=10 @ \[31\]\} @ \[33\] -do_structs::1::st \(\) -> \{.x=20 @ \[33\, 35\]\, .y=10 @ \[31\]\} @ \[33\, 35\] -do_structs::1::st \(\) -> \{.x=0 @ \[37\]\, .y=10 @ \[31\]\} @ \[37\] -do_structs::1::st \(\) -> \{.x=3 @ \[39\]\, .y=10 @ \[31\]\} @ \[39\] -do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\]\, .y=10 @ \[31\]\} @ \[39\, 41\] -do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[31\]\} @ \[39\, 41\, 44\] -do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[46\]\} @ \[46\] -do_structs::1::st \(\) -> \{.x=20 @ \[47\]\, .y=10 @ \[46\]\} @ \[47\] -do_structs::1::new_age \(\) -> \{\} @ \[48\] -do_structs::1::new_age \(\) -> \{.x=20 @ \[49\]\, .y=10 @ \[49\]\} @ \[49\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_next_thread_key \(\) -> 0ul @ \[9\] +__CPROVER_rounding_mode \(\) -> 0 @ \[10\] +__CPROVER_thread_id \(\) -> 0ul @ \[11\] +__CPROVER_threads_exited \(\) -> TOP @ \[14\] +do_structs::1::bool_ \(\) -> TOP @ \[16\] +do_structs::1::bool_1 \(\) -> TOP @ \[17\] +do_structs::1::bool_2 \(\) -> TOP @ \[18\] +do_structs::1::st \(\) -> \{\} @ \[19\] +do_structs::1::st \(\) -> \{.x=10 @ \[20\]\} @ \[20\] +do_structs::1::st \(\) -> \{.x=10 @ \[20\]\, .y=20 @ \[21\]\} @ \[21\] +do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=20 @ \[21\]\} @ \[22\] +do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=40 @ \[23\]\} @ \[23\] +do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=30 @ \[24\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=30 @ \[24\]\} @ \[25\] +do_structs::1::st \(\) -> \{.x=5 @ \[26\]\, .y=30 @ \[24\]\} @ \[26\] +do_structs::1::st \(\) -> \{.x=15 @ \[27\]\, .y=30 @ \[24\]\} @ \[27\] +do_structs::1::st \(\) -> \{.x=15 @ \[27\]\, .y=10 @ \[28\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=20 @ \[30\]\, .y=10 @ \[28\]\} @ \[30\] +do_structs::1::st \(\) -> \{.x=20 @ \[30\, 32\]\, .y=10 @ \[28\]\} @ \[30\, 32\] +do_structs::1::st \(\) -> \{.x=0 @ \[34\]\, .y=10 @ \[28\]\} @ \[34\] +do_structs::1::st \(\) -> \{.x=3 @ \[36\]\, .y=10 @ \[28\]\} @ \[36\] +do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\]\, .y=10 @ \[28\]\} @ \[36\, 38\] +do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=10 @ \[28\]\} @ \[36\, 38\, 41\] +do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=10 @ \[43\]\} @ \[43\] +do_structs::1::st \(\) -> \{.x=20 @ \[44\]\, .y=10 @ \[43\]\} @ \[44\] +do_structs::1::new_age \(\) -> \{\} @ \[45\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[46\]\, .y=10 @ \[46\]\} @ \[46\] -- 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 939236409ca..4736af6a0d8 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -4,41 +4,38 @@ sensitivity_dependency_variables.c ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_alloca_object \(\) -> TOP @ \[4\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_rounding_mode \(\) -> 0 @ \[13\] -__CPROVER_thread_id \(\) -> 0ul @ \[14\] -__CPROVER_threads_exited \(\) -> TOP @ \[17\] -global_x \(\) -> 0 @ \[18\] -do_variables::1::bool_ \(\) -> TOP @ \[20\] -do_variables::1::bool_1 \(\) -> TOP @ \[21\] -do_variables::1::bool_2 \(\) -> TOP @ \[22\] -global_x \(\) -> 5 @ \[23\] -do_variables::1::x \(\) -> TOP @ \[24\] -do_variables::1::x \(\) -> 10 @ \[25\] -do_variables::1::y \(\) -> TOP @ \[26\] -do_variables::1::y \(\) -> 20 @ \[27\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_next_thread_key \(\) -> 0ul @ \[9\] +__CPROVER_rounding_mode \(\) -> 0 @ \[10\] +__CPROVER_thread_id \(\) -> 0ul @ \[11\] +__CPROVER_threads_exited \(\) -> TOP @ \[14\] +global_x \(\) -> 0 @ \[15\] +do_variables::1::bool_ \(\) -> TOP @ \[17\] +do_variables::1::bool_1 \(\) -> TOP @ \[18\] +do_variables::1::bool_2 \(\) -> TOP @ \[19\] +global_x \(\) -> 5 @ \[20\] +do_variables::1::x \(\) -> TOP @ \[21\] +do_variables::1::x \(\) -> 10 @ \[22\] +do_variables::1::y \(\) -> TOP @ \[23\] +do_variables::1::y \(\) -> 20 @ \[24\] +do_variables::1::x \(\) -> 30 @ \[25\] +do_variables::1::y \(\) -> 40 @ \[26\] +do_variables::1::y \(\) -> 30 @ \[27\] do_variables::1::x \(\) -> 30 @ \[28\] -do_variables::1::y \(\) -> 40 @ \[29\] -do_variables::1::y \(\) -> 30 @ \[30\] -do_variables::1::x \(\) -> 30 @ \[31\] -do_variables::1::x \(\) -> 5 @ \[32\] -do_variables::1::x \(\) -> 15 @ \[33\] -do_variables::1::y \(\) -> 10 @ \[34\] -do_variables::1::x \(\) -> 20 @ \[36\] -do_variables::1::x \(\) -> 20 @ \[36\, 38\] -do_variables::1::x \(\) -> 50 @ \[40\] -do_variables::1::x \(\) -> 20 @ \[42\] -do_variables::1::x \(\) -> TOP @ \[42\, 44\] -do_variables::1::x \(\) -> 0 @ \[46\] -do_variables::1::x \(\) -> 3 @ \[48\] -do_variables::1::x \(\) -> TOP @ \[48\, 50\] -do_variables::1::x \(\) -> TOP @ \[48\, 50\, 53\] -do_variables::1::y \(\) -> 10 @ \[55\] -do_variables::1::x \(\) -> 20 @ \[56\] +do_variables::1::x \(\) -> 5 @ \[29\] +do_variables::1::x \(\) -> 15 @ \[30\] +do_variables::1::y \(\) -> 10 @ \[31\] +do_variables::1::x \(\) -> 20 @ \[33\] +do_variables::1::x \(\) -> 20 @ \[33\, 35\] +do_variables::1::x \(\) -> 50 @ \[37\] +do_variables::1::x \(\) -> 20 @ \[39\] +do_variables::1::x \(\) -> TOP @ \[39\, 41\] +do_variables::1::x \(\) -> 0 @ \[43\] +do_variables::1::x \(\) -> 3 @ \[45\] +do_variables::1::x \(\) -> TOP @ \[45\, 47\] +do_variables::1::x \(\) -> TOP @ \[45\, 47\, 50\] +do_variables::1::y \(\) -> 10 @ \[52\] +do_variables::1::x \(\) -> 20 @ \[53\] -- 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 186103d0a09..a3703a59d40 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, 51\]\[Data dependencies: 51, 2\]\[Data dominators: \], .b=.* @ \[5, 51\]\[Data dependencies: 51, 5\]\[Data dominators: \]\} @ \[2, 5, 51\]\[Data dependencies: 51, 5, 2\]\[Data dominators: 51\] -ar \(\) -> \{\[0\] = TOP @ \[11\, 45\]\[Data dependencies: 45\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 45\]\[Data dependencies: 45\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 45\]\[Data dependencies: 45\, 14\, 11\]\[Data dominators: 45\] -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: 46\] +st \(\) -> \{.a=.* @ \[2, 48\]\[Data dependencies: 48, 2\]\[Data dominators: \], .b=.* @ \[5, 48\]\[Data dependencies: 48, 5\]\[Data dominators: \]\} @ \[2, 5, 48\]\[Data dependencies: 48, 5, 2\]\[Data dominators: 48\] +ar \(\) -> \{\[0\] = TOP @ \[11\, 42\]\[Data dependencies: 42\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 42\]\[Data dependencies: 42\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 42\]\[Data dependencies: 42\, 14\, 11\]\[Data dominators: 42\] +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: 43\] -- ^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 d1be3190907..e12904c47c3 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 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 57 \[st.a\]$ -^Data dependencies: 57 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 57 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 57 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\]$ -^Data dependencies: 51 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 51 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 54 \[st.a\]$ +^Data dependencies: 54 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 54 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 54 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 54 \[st.a, st.b\]$ +^Data dependencies: 48 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 48 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 48 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 48 \[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\], 57 \[st.a\], 61 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 57 \[st.b\], 64 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\], 61 \[st.a\], 64 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\], 72 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 54 \[st.a\], 58 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 54 \[st.b\], 61 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 54 \[st.a, st.b\], 58 \[st.a\], 61 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 48 \[ar\[\([^)]*\)0\]\], 69 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 69 \[ar\[\([^)]*\)0\]\], 72 \[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 55d232cac2f..8ebc39530dd 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 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 57 \[st.a\]$ -^Data dependencies: 57 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 57 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 57 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\]$ -^Data dependencies: 51 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 54 \[st.a\]$ +^Data dependencies: 54 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 54 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 54 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 54 \[st.a, st.b\]$ +^Data dependencies: 48 \[ar\[\([^)]*\)0\]\]$ ^Data dependencies: 6 \[out1\]$ -^Data dependencies: 51 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 48 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 48 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 48 \[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\], 57 \[st.a\], 61 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 57 \[st.b\], 64 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 57 \[st.a, st.b\], 61 \[st.a\], 64 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 51 \[ar\[\([^)]*\)0\]\], 72 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 51 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 54 \[st.a\], 58 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 54 \[st.b\], 61 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 54 \[st.a, st.b\], 58 \[st.a\], 61 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 48 \[ar\[\([^)]*\)0\]\], 69 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)1\]\], 72 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 48 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 69 \[ar\[\([^)]*\)0\]\], 72 \[ar\[\([^)]*\)1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index 23d06c02fb3..9ad169f7336 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: 33 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] +\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 30 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] -- diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index a69af2a2679..6120d901d50 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -175,12 +175,9 @@ void ansi_c_internal_additions(std::string &code) // malloc "const void *" CPROVER_PREFIX "deallocated=0;\n" "const void *" CPROVER_PREFIX "dead_object=0;\n" - "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++ - CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++ "const void *" CPROVER_PREFIX "memory_leak=0;\n" "void *" CPROVER_PREFIX "allocate(" CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" - "const void *" CPROVER_PREFIX "alloca_object = 0;\n" "void " CPROVER_PREFIX "deallocate(void *);\n" CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 7b2e8f27a7d..67b70f1bac7 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -23,8 +23,6 @@ typedef signed long long __CPROVER_ssize_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); void __CPROVER_deallocate(void *); extern const void *__CPROVER_deallocated; -extern const void *__CPROVER_new_object; -extern __CPROVER_bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; extern int __CPROVER_malloc_failure_mode; diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 4928d725dcb..327ae44593a 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -108,6 +108,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); #ifndef __GNUC__ _Bool __builtin_mul_overflow(); #endif +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) { @@ -169,6 +170,9 @@ __CPROVER_HIDE:; #undef malloc __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif // malloc is marked "inline" for the benefit of goto-analyzer. Really, // goto-analyzer should take care of inlining as needed. @@ -225,7 +229,10 @@ __CPROVER_HIDE:; /* FUNCTION: __builtin_alloca */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -extern void *__CPROVER_alloca_object; +const void *__CPROVER_alloca_object = 0; +#ifndef LIBRARY_CHECK +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif void *__builtin_alloca(__CPROVER_size_t alloca_size) { @@ -265,7 +272,13 @@ __CPROVER_HIDE:; #undef free __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -extern void *__CPROVER_alloca_object; +#ifndef LIBRARY_CHECK +const void *__CPROVER_alloca_object = 0; +#endif +const void *__CPROVER_new_object = 0; +#ifndef LIBRARY_CHECK +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif void free(void *ptr) { diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 993ddc9735b..1263f509f3d 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -90,13 +90,9 @@ void cpp_internal_additions(std::ostream &out) // malloc out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n'; out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n'; - out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n'; - out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;" - << '\n'; out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n'; out << "void *" CPROVER_PREFIX "allocate(" << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n'; - out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n'; // auxiliaries for new/delete out << "void *__new(__CPROVER::size_t);" << '\n'; diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h index 7870bb31daf..cfbc3a9d4d5 100644 --- a/src/cpp/library/cprover.h +++ b/src/cpp/library/cprover.h @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com typedef __typeof__(sizeof(int)) __CPROVER_size_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); extern const void *__CPROVER_deallocated; -extern const void *__CPROVER_new_object; -extern __CPROVER_bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index 1f623058581..fd8261e47b4 100644 --- a/src/cpp/library/new.c +++ b/src/cpp/library/new.c @@ -1,6 +1,8 @@ /* FUNCTION: __new */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; inline void *__new(__typeof__(sizeof(int)) malloc_size) { @@ -25,6 +27,8 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) /* FUNCTION: __new_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) { @@ -60,6 +64,8 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p) /* FUNCTION: __delete */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; inline void __delete(void *ptr) { @@ -93,6 +99,8 @@ inline void __delete(void *ptr) /* FUNCTION: __delete_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; inline void __delete_array(void *ptr) { From d849c8f3241e07505f8aac4ad36d1ecdc41385da Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 29 Sep 2022 10:43:44 +0000 Subject: [PATCH 6/6] C library: move pthreads related definitions to library With the support of building initialisers while adding the library we can move library-only symbols to the library. This avoids polluting the initialisation function for all cases that don't actually use pthreads-related library functions. This removal of unused symbols required adding a symbol into the array_of_bool_as_bitvec test, which previously implicitly relied on those library-specific symbols in the patterns being tested for. --- .../thread_chain_cbmc1/main.c | 2 +- .../thread_chain_cbmc2/main.c | 2 +- .../cbmc/array_of_bool_as_bitvec/main.c | 1 + .../test-smt2-outfile.desc | 12 +-- regression/cbmc/xml-trace/test.desc | 2 +- regression/cprover/arrays/array1.desc | 10 +-- regression/cprover/arrays/array2.desc | 6 +- regression/cprover/basic/assume1.desc | 6 +- regression/cprover/basic/basic1.desc | 6 +- regression/cprover/basic/basic2.desc | 12 +-- regression/cprover/basic/basic3.desc | 10 +-- regression/cprover/basic/basic4.desc | 8 +- regression/cprover/basic/basic5.desc | 12 +-- regression/cprover/basic/basic6.desc | 12 +-- regression/cprover/basic/nondet1.desc | 14 ++-- regression/cprover/branching/branching1.desc | 28 +++---- regression/cprover/branching/branching2.desc | 16 ++-- regression/cprover/float/basic-float1.desc | 4 +- .../cprover/function_calls/call_no_body1.desc | 4 +- .../cprover/function_calls/call_no_body2.desc | 2 +- regression/cprover/loops/do_while1.desc | 12 +-- regression/cprover/loops/for1.desc | 16 ++-- regression/cprover/loops/for2.desc | 12 +-- regression/cprover/loops/while-break1.desc | 18 ++-- regression/cprover/pointers/malloc1.desc | 2 +- regression/cprover/pointers/pointers0.desc | 4 +- regression/cprover/pointers/pointers1.desc | 8 +- regression/cprover/pointers/pointers2.desc | 12 +-- regression/cprover/pointers/pointers3.desc | 4 +- regression/cprover/pointers/pointers4.desc | 8 +- regression/cprover/pointers/pointers5.desc | 4 +- regression/cprover/pointers/pointers6.desc | 8 +- regression/cprover/pointers/pointers7.desc | 18 ++-- regression/cprover/pointers/pointers8.desc | 6 +- regression/cprover/pointers/pointers9.desc | 8 +- .../cprover/pointers/struct_pointer1.desc | 6 +- .../cprover/pointers/struct_pointer2.desc | 6 +- .../cprover/safety/use_after_free1.desc | 4 +- .../cprover/structs/nondet_struct1.desc | 2 +- regression/cprover/structs/struct1.desc | 4 +- regression/cprover/structs/struct2.desc | 8 +- .../constant_propagation_01/test-vsd.desc | 4 +- .../constant_propagation_01/test.desc | 4 +- .../constant_propagation_02/test-vsd.desc | 4 +- .../constant_propagation_02/test.desc | 4 +- .../constant_propagation_03/test-vsd.desc | 4 +- .../constant_propagation_03/test.desc | 4 +- .../constant_propagation_04/test-vsd.desc | 4 +- .../constant_propagation_04/test.desc | 4 +- .../constant_propagation_07/test-vsd.desc | 4 +- .../constant_propagation_07/test.desc | 4 +- .../constant_propagation_08/test-vsd.desc | 4 +- .../constant_propagation_11/test-vsd.desc | 4 +- .../constant_propagation_11/test.desc | 4 +- .../constant_propagation_12/test-vsd.desc | 4 +- .../constant_propagation_12/test.desc | 4 +- .../test-liveness-show.desc | 4 +- .../test-liveness-three-way-show.desc | 4 +- .../test-write-location-show.desc | 2 +- .../test-write-location-three-way-show.desc | 2 +- .../test.desc | 43 +++++----- .../test.desc | 41 +++++----- .../test.desc | 51 ++++++------ .../test.desc | 55 ++++++------- .../test.desc | 6 +- .../test.desc | 32 ++++---- .../test.desc | 32 ++++---- .../test.desc | 2 +- src/ansi-c/ansi_c_internal_additions.cpp | 10 --- src/ansi-c/library/pthread_lib.c | 82 +++++++++++++------ src/cpp/cpp_internal_additions.cpp | 19 ----- 71 files changed, 388 insertions(+), 396 deletions(-) diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c index f9e0ab46b64..ed0471a5b18 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c +++ b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c @@ -18,7 +18,7 @@ typedef unsigned long thread_id_t; // Internal unbounded array indexed by local thread identifiers -extern __CPROVER_bool __CPROVER_threads_exited[]; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; // A thread_chain is like a chain of threads `f, g, ...` where `f` // must terminate before `g` can start to run, and so forth. diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c index f9e0ab46b64..ed0471a5b18 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c +++ b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c @@ -18,7 +18,7 @@ typedef unsigned long thread_id_t; // Internal unbounded array indexed by local thread identifiers -extern __CPROVER_bool __CPROVER_threads_exited[]; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; // A thread_chain is like a chain of threads `f, g, ...` where `f` // must terminate before `g` can start to run, and so forth. diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c index 19888bb1a45..07106dde3d2 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/main.c +++ b/regression/cbmc/array_of_bool_as_bitvec/main.c @@ -3,6 +3,7 @@ #include __CPROVER_bool w[8]; +__CPROVER_bool v[__CPROVER_constant_infinity_uint]; void main() { diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc index ae228a04e44..a7ede3fc945 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc @@ -1,15 +1,15 @@ CORE broken-smt-backend main.c --smt2 --outfile - -\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) +\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\) +\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) +\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) ^EXIT=0$ ^SIGNAL=0$ -- -\(= \(select array_of\.2 i\) false\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) false\) +\(= \(select array_of\.0 i\) false\) +\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) +\(= \(select array\.1 \(_ bv\d+ 64\)\) false\) -- This test checks for correctness of BitVec-array encoding of Boolean arrays. diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc index 5ed215d69a5..999afcec05a 100644 --- a/regression/cbmc/xml-trace/test.desc +++ b/regression/cbmc/xml-trace/test.desc @@ -7,7 +7,7 @@ activate-multi-line-match VERIFICATION FAILED