From c2890b430971ccb0c4d627d0dc9192115847f911 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Jan 2022 14:24:14 +0000 Subject: [PATCH 1/7] 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 8d6aa14c5aab2fae677df1751fd3fae2b64b6e24 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 28 Feb 2019 10:57:37 +0000 Subject: [PATCH 2/7] 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-06/test.desc | 4 +- regression/cbmc-library/memcpy-07/main.c | 1 + .../cbmc/String_Abstraction17/test.desc | 2 +- .../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 | 125 ++++++++++++++---- src/goto-programs/link_to_library.h | 7 +- 12 files changed, 121 insertions(+), 40 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-06/test.desc b/regression/cbmc-library/memcpy-06/test.desc index ab649ecc026..c0abaeddc09 100644 --- a/regression/cbmc-library/memcpy-06/test.desc +++ b/regression/cbmc-library/memcpy-06/test.desc @@ -2,8 +2,8 @@ CORE main.c function 'memcpy' is not declared -parameter "memcpy::dst" type mismatch -^EXIT=6$ +Linking library function 'memcpy' failed +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring 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/test.desc b/regression/cbmc/String_Abstraction17/test.desc index ea2896bae68..9e85c0c54ed 100644 --- a/regression/cbmc/String_Abstraction17/test.desc +++ b/regression/cbmc/String_Abstraction17/test.desc @@ -1,7 +1,7 @@ CORE strcpy-no-decl.c --string-abstraction --validate-goto-model -Condition: strlen type inconsistency +^Condition: fct_type.parameters\(\).size\(\) == parameter_identifiers.size\(\)$ ^EXIT=(127|134)$ ^SIGNAL=0$ -- 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 1c080c84ccd..ffe6ec1418d 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 17386f3d457..45989869aa6 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -94,7 +94,8 @@ std::string get_cprover_library_text( void cprover_c_library_factory( const std::set &functions, - symbol_tablet &symbol_table, + const symbol_tablet &symbol_table, + symbol_tablet &dest_symbol_table, message_handlert &message_handler) { if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE) @@ -104,7 +105,7 @@ void cprover_c_library_factory( 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); } void add_library( diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index 8a7804113b6..84b1eeffaa0 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -36,6 +36,7 @@ void add_library( void cprover_c_library_factory( const std::set &functions, + const symbol_tablet &, symbol_tablet &, message_handlert &); diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp index fae330e1063..b5425b3dcc3 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_tablet &symbol_table, + const symbol_tablet &symbol_table, + symbol_tablet &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 9f08436a2fe..c572fb597b3 100644 --- a/src/cpp/cprover_library.h +++ b/src/cpp/cprover_library.h @@ -18,6 +18,7 @@ class symbol_tablet; void cprover_cpp_library_factory( const std::set &functions, + const symbol_tablet &, symbol_tablet &, message_handlert &); diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 48b18553bb5..353fc8a4fd9 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -14,6 +14,60 @@ Author: Daniel Kroening, kroening@kroening.com #include "compute_called_functions.h" #include "goto_convert_functions.h" #include "goto_model.h" +#include "link_goto_model.h" + +#include + +/// 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 @@ -25,24 +79,27 @@ Author: Daniel Kroening, kroening@kroening.com 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; + 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 +116,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 bcfe0c8b2531ae59355e21bd5e367f5046e19a8d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 17 Jan 2022 21:07:00 +0000 Subject: [PATCH 3/7] 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. --- .../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 -- 31 files changed, 163 insertions(+), 175 deletions(-) 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 ccd63713bc4..98e9976bd49 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: 2, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 7, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 14, 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 1c39cb67b5c..0745b4c86cc 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -206,11 +206,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 beeb1501d9a..e4f68f9af47 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); extern const void *__CPROVER_deallocated; extern const void *__CPROVER_new_object; diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 096d8f9837d..f2c4408e5ed 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(); @@ -96,7 +96,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; @@ -148,7 +148,7 @@ inline 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; @@ -222,7 +222,7 @@ inline 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 f8776294de063a739817650d0f67d745777706d0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Jan 2022 15:08:33 +0000 Subject: [PATCH 4/7] 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/free-01/test.desc | 2 +- .../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 +++ 34 files changed, 210 insertions(+), 209 deletions(-) diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc index 769ba573e7c..a727d0817d0 100644 --- a/regression/cbmc-library/free-01/test.desc +++ b/regression/cbmc-library/free-01/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --bounds-check --stop-on-fail -free argument must be NULL or valid pointer +free argument must be (NULL or valid pointer|dynamic object) ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ 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 98e9976bd49..8574c3a6aeb 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: 2, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 3, 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 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 0745b4c86cc..02a0ec31361 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -173,12 +173,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" CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ integer2string(max_malloc_size(config.ansi_c.pointer_width, config diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index e4f68f9af47..7b88f7cf65a 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -22,8 +22,6 @@ typedef signed long long __CPROVER_ssize_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; extern int __CPROVER_malloc_failure_mode; diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index bb3cd940290..f96e3edf89d 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -71,6 +71,7 @@ inline void abort(void) #undef calloc __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +_Bool __CPROVER_malloc_is_new_array = 0; inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) { @@ -141,6 +142,9 @@ __CPROVER_HIDE:; #undef malloc __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline void *malloc(__CPROVER_size_t malloc_size) { @@ -199,7 +203,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 +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline void *__builtin_alloca(__CPROVER_size_t alloca_size) { @@ -242,7 +249,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 +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline 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 a89d9dce8d0..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 _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 d0dcde466d1..6a549379924 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; +_Bool __CPROVER_malloc_is_new_array = 0; inline void *__new(__typeof__(sizeof(int)) malloc_size) { @@ -28,6 +30,8 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) /* FUNCTION: __new_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) { @@ -66,6 +70,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; +_Bool __CPROVER_malloc_is_new_array = 0; inline void __delete(void *ptr) { @@ -101,6 +107,8 @@ inline void __delete(void *ptr) /* FUNCTION: __delete_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void __delete_array(void *ptr) { From c3f5f03689b8e5f3bf27c7abce65d8189f366040 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Jan 2022 11:40:31 +0000 Subject: [PATCH 5/7] 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 +-- .../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 | 78 +++++++++++++------ src/cpp/cpp_internal_additions.cpp | 19 ----- 34 files changed, 223 insertions(+), 235 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/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc index d498e0b409c..741965ab2a5 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: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, 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 a4a79f28ab1..e0147b4ce18 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: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, 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 4d18142ff67..db447649547 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 6a28820a4b0..f8465991235 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 4d18142ff67..db447649547 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 6a28820a4b0..f8465991235 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 4d18142ff67..db447649547 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 6a28820a4b0..f8465991235 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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 46bac02fac4..14364a509af 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: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, 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_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 87b2c5112b0..3b836b8dad2 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: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, 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_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index 8574c3a6aeb..bd028bcc6c5 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: 2, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 9, 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 ba1ee57a8f7..90e1b48f887 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, 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 6653d122562..bba19b94b66 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, 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 2f4f1e9d2b4..e8b6c2d034f 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: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, 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 df5dd997788..614698c7277 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: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, 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 f8ae2826abc..c1501370247 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 @ \[21\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[24\] +globalX .* TOP @ \[18\] -- 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 6a38f8f90a0..2c13d44ae4b 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 @ \[21\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[24\] +globalX .* TOP @ \[18\] -- 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 d0ab8a1918d..f3fd23e0665 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 @ \[21\] +globalX .* 0 @ \[15\] 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 2f78ad7aaba..242a87dda34 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 @ \[21\] +globalX .* 0 @ \[15\] 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 b698835de22..19398dce8fb 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -9,26 +9,23 @@ main#return_value \(\) -> TOP @ \[1\] __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\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_arrays::1::bool_ \(\) -> TOP @ \[10\] +do_arrays::1::bool_1 \(\) -> TOP @ \[11\] +do_arrays::1::bool_2 \(\) -> TOP @ \[12\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\] 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 b1d1e153d43..94a6ad7e383 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -9,25 +9,22 @@ main#return_value \(\) -> TOP @ \[1\] __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\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_pointers::1::bool_ \(\) -> TOP @ \[10\] +do_pointers::1::bool_1 \(\) -> TOP @ \[11\] +do_pointers::1::bool_2 \(\) -> TOP @ \[12\] +do_pointers::1::x \(\) -> TOP @ \[13\] +do_pointers::1::x \(\) -> 10 @ \[14\] +do_pointers::1::x_p \(\) -> TOP @ \[15\] +do_pointers::1::y \(\) -> TOP @ \[16\] +do_pointers::1::y \(\) -> 20 @ \[17\] +do_pointers::1::y_p \(\) -> TOP @ \[18\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\] +do_pointers::1::x \(\) -> 30 @ \[20\] +do_pointers::1::x \(\) -> 40 @ \[21\] +do_pointers::1::x \(\) -> TOP @ \[22\] +do_pointers::1::x \(\) -> 50 @ \[23\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\] +do_pointers::1::x \(\) -> 60 @ \[25\] +do_pointers::1::j \(\) -> TOP @ \[26\] +do_pointers::1::j \(\) -> 60 @ \[27\] 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 0d84d60671a..c74416efa88 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -9,31 +9,28 @@ main#return_value \(\) -> TOP @ \[1\] __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\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_structs::1::bool_ \(\) -> TOP @ \[10\] +do_structs::1::bool_1 \(\) -> TOP @ \[11\] +do_structs::1::bool_2 \(\) -> TOP @ \[12\] +do_structs::1::st \(\) -> \{\} @ \[13\] +do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\] +do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\] +do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\] +do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\] +do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\] +do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\] +do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\] +do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\] +do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\] +do_structs::1::new_age \(\) -> \{\} @ \[39\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\] -- 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 4736af6a0d8..ccb6a2526dc 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -7,35 +7,32 @@ main#return_value \(\) -> TOP @ \[1\] __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::x \(\) -> 5 @ \[29\] -do_variables::1::x \(\) -> 15 @ \[30\] -do_variables::1::y \(\) -> 10 @ \[31\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +global_x \(\) -> 0 @ \[9\] +do_variables::1::bool_ \(\) -> TOP @ \[11\] +do_variables::1::bool_1 \(\) -> TOP @ \[12\] +do_variables::1::bool_2 \(\) -> TOP @ \[13\] +global_x \(\) -> 5 @ \[14\] +do_variables::1::x \(\) -> TOP @ \[15\] +do_variables::1::x \(\) -> 10 @ \[16\] +do_variables::1::y \(\) -> TOP @ \[17\] +do_variables::1::y \(\) -> 20 @ \[18\] +do_variables::1::x \(\) -> 30 @ \[19\] +do_variables::1::y \(\) -> 40 @ \[20\] +do_variables::1::y \(\) -> 30 @ \[21\] +do_variables::1::x \(\) -> 30 @ \[22\] +do_variables::1::x \(\) -> 5 @ \[23\] +do_variables::1::x \(\) -> 15 @ \[24\] +do_variables::1::y \(\) -> 10 @ \[25\] +do_variables::1::x \(\) -> 20 @ \[27\] +do_variables::1::x \(\) -> 20 @ \[27\, 29\] +do_variables::1::x \(\) -> 50 @ \[31\] do_variables::1::x \(\) -> 20 @ \[33\] -do_variables::1::x \(\) -> 20 @ \[33\, 35\] -do_variables::1::x \(\) -> 50 @ \[37\] -do_variables::1::x \(\) -> 20 @ \[39\] +do_variables::1::x \(\) -> TOP @ \[33\, 35\] +do_variables::1::x \(\) -> 0 @ \[37\] +do_variables::1::x \(\) -> 3 @ \[39\] do_variables::1::x \(\) -> TOP @ \[39\, 41\] -do_variables::1::x \(\) -> 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\] +do_variables::1::x \(\) -> TOP @ \[39\, 41\, 44\] +do_variables::1::y \(\) -> 10 @ \[46\] +do_variables::1::x \(\) -> 20 @ \[47\] -- 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 a3703a59d40..a87879274f8 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, 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\] +st \(\) -> \{.a=.* @ \[2, 42\]\[Data dependencies: 42, 2\]\[Data dominators: \], .b=.* @ \[5, 42\]\[Data dependencies: 42, 5\]\[Data dominators: \]\} @ \[2, 5, 42\]\[Data dependencies: 42, 5, 2\]\[Data dominators: 42\] +ar \(\) -> \{\[0\] = TOP @ \[11\, 36\]\[Data dependencies: 36\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 36\]\[Data dependencies: 36\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 36\]\[Data dependencies: 36\, 14\, 11\]\[Data dominators: 36\] +arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 37\] -- ^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 e12904c47c3..cd3a57851d6 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: 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: 48 \[st.a\]$ +^Data dependencies: 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ -^Data dependencies: 1 \[st.a\], 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\]\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ -- ^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 8ebc39530dd..8abe0ffdcec 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: 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 \[st.a\]$ +^Data dependencies: 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ ^Data dependencies: 6 \[out1\]$ -^Data dependencies: 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: 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ -^Data dependencies: 1 \[st.a\], 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\]\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ -- ^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 9ad169f7336..8bae062cd04 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: 30 \[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: 24 \[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 02a0ec31361..d811fbadbbb 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -157,16 +157,6 @@ void ansi_c_internal_additions(std::string &code) "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n" "typedef void " CPROVER_PREFIX "integer;\n" "typedef void " CPROVER_PREFIX "rational;\n" - CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n" - CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited[" - CPROVER_PREFIX "constant_infinity_uint];\n" - "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n" - CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys[" - CPROVER_PREFIX "constant_infinity_uint];\n" - CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors[" - CPROVER_PREFIX "constant_infinity_uint])(void *);\n" - CPROVER_PREFIX "thread_local unsigned long " - CPROVER_PREFIX "next_thread_key = 0;\n" "extern unsigned char " CPROVER_PREFIX "memory[" CPROVER_PREFIX "constant_infinity_uint];\n" diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 849f217472f..73ac2892ffa 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -290,12 +290,15 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex) #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; - -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#if 0 +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif inline void pthread_exit(void *value_ptr) { @@ -331,9 +334,11 @@ inline void pthread_exit(void *value_ptr) #define __CPROVER_ERRNO_H_INCLUDED #endif -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; -extern unsigned long __CPROVER_next_thread_id; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#endif +unsigned long __CPROVER_next_thread_id = 0; inline int pthread_join(pthread_t thread, void **value_ptr) { @@ -368,9 +373,11 @@ __CPROVER_HIDE:; #endif #ifdef __APPLE__ -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; -extern unsigned long __CPROVER_next_thread_id; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +unsigned long __CPROVER_next_thread_id = 0; +#endif inline int _pthread_join(pthread_t thread, void **value_ptr) { @@ -533,12 +540,17 @@ inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock) /* FUNCTION: __spawned_thread */ -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; - -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#endif +#if 0 +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +#endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; inline void __spawned_thread( unsigned long this_thread_id, @@ -596,7 +608,14 @@ __CPROVER_HIDE:; # define __CPROVER_PTHREAD_H_INCLUDED #endif -extern unsigned long __CPROVER_next_thread_id; +#ifndef LIBRARY_CHECK +unsigned long __CPROVER_next_thread_id = 0; +# if 0 +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +# endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif void __spawned_thread( unsigned long this_thread_id, @@ -932,9 +951,15 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier) #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +# if 0 +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +# endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) { @@ -958,7 +983,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline int pthread_key_delete(pthread_key_t key) { @@ -974,7 +1000,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline void *pthread_getspecific(pthread_key_t key) { @@ -989,7 +1016,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline int pthread_setspecific(pthread_key_t key, const void *value) { diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 1263f509f3d..aae4a67dbff 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -67,25 +67,6 @@ void cpp_internal_additions(std::ostream &out) out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n'; out << "typedef void " CPROVER_PREFIX "integer;" << '\n'; out << "typedef void " CPROVER_PREFIX "rational;" << '\n'; - // TODO: thread_local is still broken - // out << "thread_local unsigned long " - // << CPROVER_PREFIX "thread_id = 0;" << '\n'; - out << CPROVER_PREFIX "bool " - << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];" - << '\n'; - out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n'; - // TODO: thread_local is still broken - out << "void* " - << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];" - << '\n'; - // TODO: thread_local is still broken - out << "void (*" - << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])" - << "(void *);" << '\n'; - // TODO: thread_local is still broken - out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n'; - out << "extern unsigned char " - << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; // malloc out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n'; From dcdf046ecb568e84bda65528cf16b481b3e28fb1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Nov 2020 00:53:06 +0000 Subject: [PATCH 6/7] Invoke functions marked __attribute__((destructor)) This is a GCC extension that our front-end parses, but an implementation of the desired semantics was hitherto missing. --- regression/cbmc/destructor1/main.c | 17 +++++++++++++++++ regression/cbmc/destructor1/test.desc | 9 +++++++++ src/ansi-c/ansi_c_entry_point.cpp | 20 ++++++++++++++++++++ 3 files changed, 46 insertions(+) create mode 100644 regression/cbmc/destructor1/main.c create mode 100644 regression/cbmc/destructor1/test.desc diff --git a/regression/cbmc/destructor1/main.c b/regression/cbmc/destructor1/main.c new file mode 100644 index 00000000000..275e04de283 --- /dev/null +++ b/regression/cbmc/destructor1/main.c @@ -0,0 +1,17 @@ +#include + +#ifdef __GNUC__ +static __attribute__((destructor)) void assert_false(void) +{ + assert(0); +} +#endif + +int main() +{ +#ifndef __GNUC__ + // explicitly invoke assert_false as __attribute__((destructor)) isn't + // supported + assert_false(); +#endif +} diff --git a/regression/cbmc/destructor1/test.desc b/regression/cbmc/destructor1/test.desc new file mode 100644 index 00000000000..7a0fc8c72e1 --- /dev/null +++ b/regression/cbmc/destructor1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^\[assert_false.assertion.1\] line 7 assertion 0: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 41f134b6f1b..bf2c92ee637 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -504,6 +504,26 @@ bool generate_ansi_c_start_function( record_function_outputs(symbol, init_code, symbol_table); + // now call destructor functions (a GCC extension) + + for(const auto &symbol_table_entry : symbol_table.symbols) + { + const symbolt &symbol = symbol_table_entry.second; + + if(symbol.type.id() != ID_code) + continue; + + const code_typet &code_type = to_code_type(symbol.type); + if( + code_type.return_type().id() == ID_destructor && + code_type.parameters().empty()) + { + code_function_callt function_call(symbol.symbol_expr()); + function_call.add_source_location() = symbol.location; + init_code.add(std::move(function_call)); + } + } + // add the entry point symbol symbolt new_symbol; From 8edaf8e984c6fc6491c57a80aed97b3676eb6235 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Nov 2020 01:05:36 +0000 Subject: [PATCH 7/7] C library: atexit atexit introduces function calls that may affect the verification outcome. --- regression/cbmc-library/atexit-01/main.c | 12 +++++ regression/cbmc-library/atexit-01/test.desc | 8 ++++ regression/cbmc-library/atexit-02/main.c | 13 ++++++ regression/cbmc-library/atexit-02/test.desc | 8 ++++ .../cbmc-library/posix_memalign-02/test.desc | 1 + .../pthread_cond_wait-01/test.desc | 2 +- .../Pointer_byte_extract5/no-simplify.desc | 2 +- .../cbmc/array-cell-sensitivity2/test.desc | 2 +- regression/cbmc/array_constraints1/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 2 +- .../cbmc/multiple-goto-traces/test.desc | 2 +- regression/cbmc/pragma_cprover1/test.desc | 2 +- regression/cbmc/pragma_cprover2/test.desc | 2 +- regression/cbmc/switch8/test.desc | 2 +- regression/cbmc/union12/test.desc | 2 +- src/analyses/goto_check_c.cpp | 45 +++++++++---------- src/ansi-c/ansi_c_entry_point.cpp | 19 +++++++- src/ansi-c/ansi_c_internal_additions.cpp | 3 ++ src/ansi-c/library/stdlib.c | 36 +++++++++++++++ src/cpp/cpp_internal_additions.cpp | 3 ++ src/linking/remove_internal_symbols.cpp | 1 + 21 files changed, 134 insertions(+), 35 deletions(-) create mode 100644 regression/cbmc-library/atexit-01/main.c create mode 100644 regression/cbmc-library/atexit-01/test.desc create mode 100644 regression/cbmc-library/atexit-02/main.c create mode 100644 regression/cbmc-library/atexit-02/test.desc diff --git a/regression/cbmc-library/atexit-01/main.c b/regression/cbmc-library/atexit-01/main.c new file mode 100644 index 00000000000..40ee8f2201b --- /dev/null +++ b/regression/cbmc-library/atexit-01/main.c @@ -0,0 +1,12 @@ +#include +#include + +void cleanup() +{ + assert(0); +} + +int main() +{ + atexit(cleanup); +} diff --git a/regression/cbmc-library/atexit-01/test.desc b/regression/cbmc-library/atexit-01/test.desc new file mode 100644 index 00000000000..4b9176a942e --- /dev/null +++ b/regression/cbmc-library/atexit-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --bounds-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/atexit-02/main.c b/regression/cbmc-library/atexit-02/main.c new file mode 100644 index 00000000000..696dc20eed0 --- /dev/null +++ b/regression/cbmc-library/atexit-02/main.c @@ -0,0 +1,13 @@ +#include +#include + +void cleanup() +{ + assert(0); +} + +int main() +{ + atexit(cleanup); + exit(0); +} diff --git a/regression/cbmc-library/atexit-02/test.desc b/regression/cbmc-library/atexit-02/test.desc new file mode 100644 index 00000000000..4b9176a942e --- /dev/null +++ b/regression/cbmc-library/atexit-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --bounds-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/posix_memalign-02/test.desc b/regression/cbmc-library/posix_memalign-02/test.desc index 648263292fe..8a67b803b89 100644 --- a/regression/cbmc-library/posix_memalign-02/test.desc +++ b/regression/cbmc-library/posix_memalign-02/test.desc @@ -6,5 +6,6 @@ main.c ^VERIFICATION FAILED$ \[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE \[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE +\*\* 2 of 24 failed -- ^warning: ignoring diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc index adbd7d687d0..2a2cb693e76 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/test.desc +++ b/regression/cbmc-library/pthread_cond_wait-01/test.desc @@ -3,7 +3,7 @@ main.c --bounds-check ^EXIT=10$ ^SIGNAL=0$ -^\*\* 1 of 2 failed +^\*\* 1 of 4 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index 31b58b17b85..23f8cefebfe 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed +\*\* 1 of 18 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc index 65b734796e9..429cfbdd7fc 100644 --- a/regression/cbmc/array-cell-sensitivity2/test.desc +++ b/regression/cbmc/array-cell-sensitivity2/test.desc @@ -6,7 +6,7 @@ main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\) ^EXIT=0$ ^SIGNAL=0$ -- -\[\[[0-9]+\]\] +array.*\[\[[0-9]+\]\] -- This checks that arrays of uncertain size are always treated as aggregates and are not expanded into individual cell symbols (which use the [[index]] notation diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 8040e5651bf..d38dbc8f225 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 14 +^\*\* 2 of 24 -- ^warning: ignoring diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index c88637311c2..aa85298ef8b 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ ^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ -^\*\* 1 of 6 failed +^\*\* 2 of 9 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc index f5009b36556..46ea40d5c4b 100644 --- a/regression/cbmc/multiple-goto-traces/test.desc +++ b/regression/cbmc/multiple-goto-traces/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -Trace for main\.assertion\.1:(\n.*){22} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50} assertion argc \+ 1 != 5 +Trace for main\.assertion\.1:(\n.*){150} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){164} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){178} assertion argc \+ 1 != 5 \*\* 3 of 4 failed -- ^warning: ignoring diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 2ed565c0062..3ea73ad9572 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -2,7 +2,7 @@ CORE main.c --signed-overflow-check --bounds-check line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ -^\*\* 1 of 1 failed +^\*\* 1 of 4 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc index fc1f888dfcf..249a0cae2c6 100644 --- a/regression/cbmc/pragma_cprover2/test.desc +++ b/regression/cbmc/pragma_cprover2/test.desc @@ -3,7 +3,7 @@ main.c --signed-overflow-check ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$ ^\[main.overflow\.2\] line 22 arithmetic overflow on signed \+ in x \+ n: FAILURE$ -^\*\* 2 of 2 failed +^\*\* 2 of 3 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc index 62e8b9730ae..5b963c0786f 100644 --- a/regression/cbmc/switch8/test.desc +++ b/regression/cbmc/switch8/test.desc @@ -13,7 +13,7 @@ main.c ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$ ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$ ^\[main\.assertion\.5\] line 51 assertion f == 42: FAILURE$ -^\*\* 4 of 10 failed +^\*\* 4 of 18 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc index 6b04b86af6e..64dc24e15f6 100644 --- a/regression/cbmc/union12/test.desc +++ b/regression/cbmc/union12/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] line 20 should fail: FAILURE$ -^\*\* 1 of 15 failed +^\*\* 1 of 25 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index dff22d10b3d..43e95c28aaa 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -2213,6 +2213,28 @@ void goto_check_ct::goto_check( i.turn_into_skip(); did_something = true; } + + if(enable_memory_leak_check && function_identifier == "exit") + { + const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); + const symbol_exprt leak_expr = leak.symbol_expr(); + + // add self-assignment to get helpful counterexample output + new_code.add(goto_programt::make_assignment(leak_expr, leak_expr)); + + source_locationt source_location; + source_location.set_function(function_identifier); + + equal_exprt eq( + leak_expr, null_pointer_exprt(to_pointer_type(leak.type))); + add_guarded_property( + eq, + "dynamically allocated memory never freed", + "memory-leak", + source_location, + eq, + identity); + } } else if(i.is_dead()) { @@ -2262,29 +2284,6 @@ void goto_check_ct::goto_check( } else if(i.is_end_function()) { - if( - function_identifier == goto_functionst::entry_point() && - enable_memory_leak_check) - { - const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); - const symbol_exprt leak_expr = leak.symbol_expr(); - - // add self-assignment to get helpful counterexample output - new_code.add(goto_programt::make_assignment(leak_expr, leak_expr)); - - source_locationt source_location; - source_location.set_function(function_identifier); - - equal_exprt eq( - leak_expr, null_pointer_exprt(to_pointer_type(leak.type))); - add_guarded_property( - eq, - "dynamically allocated memory never freed", - "memory-leak", - source_location, - eq, - identity); - } } for(auto &instruction : new_code.instructions) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index bf2c92ee637..1f520ab1fd3 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -242,6 +242,8 @@ bool generate_ansi_c_start_function( const code_typet::parameterst ¶meters= to_code_type(symbol.type).parameters(); + const namespacet ns(symbol_table); + if(symbol.name==ID_main) { if(parameters.empty()) @@ -250,8 +252,6 @@ bool generate_ansi_c_start_function( } else if(parameters.size()==2 || parameters.size()==3) { - namespacet ns(symbol_table); - { symbolt argc_symbol; @@ -498,8 +498,23 @@ bool generate_ansi_c_start_function( parameters, init_code, symbol_table, object_factory_parameters); } + exprt return_value = call_main.lhs(); init_code.add(std::move(call_main)); + const symbolt &exit_symbol = ns.lookup("exit"); + const typet &arg_type = to_code_type(exit_symbol.type).parameters()[0].type(); + code_function_callt call_exit{exit_symbol.symbol_expr()}; + if(return_value.is_not_nil()) + { + call_exit.arguments().push_back( + typecast_exprt::conditional_cast(return_value, arg_type)); + } + else + call_exit.arguments().push_back(from_integer(0, arg_type)); + call_exit.add_source_location() = symbol.location; + call_exit.function().add_source_location() = symbol.location; + init_code.add(std::move(call_exit)); + // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT record_function_outputs(symbol, init_code, symbol_table); diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index d811fbadbbb..1e75d51c01f 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -186,6 +186,9 @@ void ansi_c_internal_additions(std::string &code) id2string(rounding_mode_identifier()) + '='+ std::to_string(config.ansi_c.rounding_mode)+";\n" + // atexit + "void exit(int);\n" + // pipes, write, read, close "struct " CPROVER_PREFIX "pipet {\n" " _Bool widowed;\n" diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index f96e3edf89d..28d7bd4eac1 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -32,9 +32,20 @@ inline long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i #undef exit +__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void); +__CPROVER_thread_local int __CPROVER_atexit_table_use = 0; + inline void exit(int status) { +__CPROVER_HIDE:; (void)status; + + while(__CPROVER_atexit_table_use > 0) + { + --__CPROVER_atexit_table_use; + __CPROVER_atexit_table[__CPROVER_atexit_table_use](); + } + __CPROVER_assume(0); #ifdef LIBRARY_CHECK __builtin_unreachable(); @@ -604,3 +615,28 @@ __CPROVER_HIDE:; __CPROVER_assume(result >= 0); return result; } + +/* FUNCTION: atexit */ + +#ifndef __CPROVER_ERRNO_H_INCLUDED +# include +# define __CPROVER_ERRNO_H_INCLUDED +#endif + +#ifndef LIBRARY_CHECK +__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void); +__CPROVER_thread_local int __CPROVER_atexit_table_use = 0; +#endif + +int atexit(void (*function)(void)) +{ +__CPROVER_HIDE:; + if(__CPROVER_atexit_table_use >= 32) + { + errno = ENOMEM; + return -1; + } + + __CPROVER_atexit_table[__CPROVER_atexit_table_use++] = function; + return 0; +} diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index aae4a67dbff..704587d80a3 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -89,6 +89,9 @@ void cpp_internal_additions(std::ostream &out) out << "int " << rounding_mode_identifier() << " = " << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n'; + // atexit + out << "void exit(int);" << '\n'; + // pipes, write, read, close out << "struct " CPROVER_PREFIX "pipet {\n" << " bool widowed;\n" diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 5258d149210..44a6c1be716 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -127,6 +127,7 @@ void remove_internal_symbols( special.insert("__placement_new_array"); special.insert("__delete"); special.insert("__delete_array"); + special.insert("exit"); for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin();