diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc index 621decdd139..78c0bc19716 100644 --- a/regression/goto-harness/havoc-global-int-01/test.desc +++ b/regression/goto-harness/havoc-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 --havoc-variables x +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 --havoc-variables x ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc index a1243f319fc..5617b1ecfcd 100644 --- a/regression/goto-harness/havoc-global-int-02/test.desc +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-location main:9 --havoc-variables y +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ ^EXIT=10$ diff --git a/regression/goto-harness/havoc-global-int-03/main.c b/regression/goto-harness/havoc-global-int-03/main.c new file mode 100644 index 00000000000..920f3f063aa --- /dev/null +++ b/regression/goto-harness/havoc-global-int-03/main.c @@ -0,0 +1,10 @@ +int x = 1; + +int main() +{ + assert(x == 1); //unreachable, hence success + assert(x == 2); + assert(x == 3); + + return 0; +} diff --git a/regression/goto-harness/havoc-global-int-03/test.desc b/regression/goto-harness/havoc-global-int-03/test.desc new file mode 100644 index 00000000000..941b9dd7054 --- /dev/null +++ b/regression/goto-harness/havoc-global-int-03/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion x == 2: FAILURE +\[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc index 4d85c4c6be7..a8c4a8110dc 100644 --- a/regression/goto-harness/havoc-global-struct/test.desc +++ b/regression/goto-harness/havoc-global-struct/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-location main:3 --havoc-variables simple +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$ diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc index d05e4853896..427e39149b9 100644 --- a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:1 +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc index 8092fa6d9f6..dcdca581119 100644 --- a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-location main:0 +--harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc index 1e064294660..b6d37979434 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc index db97cfec79c..52735e239fa 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc index 1e064294660..b6d37979434 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc index d05e4853896..427e39149b9 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:1 +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc index 8092fa6d9f6..dcdca581119 100644 --- a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-location main:0 +--harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index d4451d044cc..b313e8fdc80 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -6,6 +6,8 @@ Author: Daniel Poetzl \******************************************************************/ +#include + #include "memory_snapshot_harness_generator.h" #include @@ -34,33 +36,18 @@ void memory_snapshot_harness_generatort::handle_option( { memory_snapshot_file = require_exactly_one_value(option, values); } - else if(option == "initial-location") + else if(option == "initial-goto-location") { - const std::string initial_location = - require_exactly_one_value(option, values); - - std::vector start; - split_string(initial_location, ':', start, true); - - if( - start.empty() || start.front().empty() || - (start.size() == 2 && start.back().empty()) || start.size() > 2) - { - throw invalid_command_line_argument_exceptiont( - "invalid initial location specification", "--initial-location"); - } - - entry_function_name = start.front(); - - if(start.size() == 2) - { - location_number = optionalt(safe_string2unsigned(start.back())); - } + initial_goto_location_line = require_exactly_one_value(option, values); } else if(option == "havoc-variables") { variables_to_havoc.insert(values.begin(), values.end()); } + else if(option == "initial-source-location") + { + initial_source_location_line = require_exactly_one_value(option, values); + } else { throw invalid_command_line_argument_exceptiont( @@ -79,106 +66,51 @@ void memory_snapshot_harness_generatort::validate_options( "--harness-type initialise-from-memory-snapshot"); } - if(entry_function_name.empty()) + if(initial_source_location_line.empty() == initial_goto_location_line.empty()) { - INVARIANT( - !location_number.has_value(), - "when `function` is empty then the option --initial-location was not " - "given and thus `location_number` was not set"); - throw invalid_command_line_argument_exceptiont( - "option --initial-location is required", - "--harness-type initialise-from-memory-snapshot"); + "choose either source or goto location to specify the entry point", + "--initial-source/goto-location"); } - const auto &goto_functions = goto_model.goto_functions; - const auto &goto_function = - goto_functions.function_map.find(entry_function_name); - if(goto_function == goto_functions.function_map.end()) - { - throw invalid_command_line_argument_exceptiont( - "unknown initial location specification", "--initial-location"); - } - - if(!goto_function->second.body_available()) + if(!initial_source_location_line.empty()) { - throw invalid_command_line_argument_exceptiont( - "given function `" + id2string(entry_function_name) + - "` does not have a body", - "--initial-location"); + entry_location = initialize_entry_via_source( + parse_source_location(initial_source_location_line), + goto_model.goto_functions); } - - if(location_number.has_value()) - { - const auto &goto_program = goto_function->second.body; - const auto opt_it = goto_program.get_target(*location_number); - - if(!opt_it.has_value()) - { - throw invalid_command_line_argument_exceptiont( - "no instruction with location number " + - std::to_string(*location_number) + " in function " + - id2string(entry_function_name), - "--initial-location"); - } - } - - if(goto_functions.function_map.count(INITIALIZE_FUNCTION) == 0) + else { - throw invalid_command_line_argument_exceptiont( - "invalid input program: " + std::string(INITIALIZE_FUNCTION) + - " not found", - ""); + entry_location = initialize_entry_via_goto( + parse_goto_location(initial_goto_location_line), + goto_model.goto_functions); } const symbol_tablet &symbol_table = goto_model.symbol_table; + const symbolt *called_function_symbol = - symbol_table.lookup(entry_function_name); + symbol_table.lookup(entry_location.function_name); if(called_function_symbol == nullptr) { throw invalid_command_line_argument_exceptiont( - "function `" + id2string(entry_function_name) + + "function `" + id2string(entry_location.function_name) + "` not found in the symbol table", "--initial-location"); } } void memory_snapshot_harness_generatort::add_init_section( + const symbol_exprt &func_init_done_var, goto_modelt &goto_model) const { goto_functionst &goto_functions = goto_model.goto_functions; - symbol_tablet &symbol_table = goto_model.symbol_table; goto_functiont &goto_function = - goto_functions.function_map[entry_function_name]; - const symbolt &function_symbol = symbol_table.lookup_ref(entry_function_name); + goto_functions.function_map[entry_location.function_name]; goto_programt &goto_program = goto_function.body; - // introduce a symbol for a Boolean variable to indicate the point at which - // the function initialisation is completed - symbolt &func_init_done_symbol = get_fresh_aux_symbol( - bool_typet(), - id2string(entry_function_name), - "func_init_done", - function_symbol.location, - function_symbol.mode, - symbol_table); - func_init_done_symbol.is_static_lifetime = true; - func_init_done_symbol.value = false_exprt(); - - const symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr(); - - // initialise func_init_done_var in __CPROVER_initialize if it is present - // so that it's FALSE value is visible before the harnessed function is called - goto_programt &cprover_initialize = - goto_functions.function_map.find(INITIALIZE_FUNCTION)->second.body; - cprover_initialize.insert_before( - std::prev(cprover_initialize.instructions.end()), - goto_programt::make_assignment( - code_assignt(func_init_done_var, false_exprt()))); - const goto_programt::const_targett start_it = goto_program.instructions.begin(); @@ -195,9 +127,8 @@ void memory_snapshot_harness_generatort::add_init_section( goto_program.compute_location_numbers(); goto_program.insert_after( ins_it2, - goto_programt::make_goto(goto_program.const_cast_target( - location_number.has_value() ? *goto_program.get_target(*location_number) - : start_it))); + goto_programt::make_goto( + goto_program.const_cast_target(entry_location.start_instruction))); } code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( @@ -323,13 +254,28 @@ void memory_snapshot_harness_generatort::generate( goto_functionst &goto_functions = goto_model.goto_functions; const symbolt *called_function_symbol = - symbol_table.lookup(entry_function_name); + symbol_table.lookup(entry_location.function_name); - add_init_section(goto_model); + // introduce a symbol for a Boolean variable to indicate the point at which + // the function initialisation is completed + auto &func_init_done_symbol = get_fresh_aux_symbol( + bool_typet(), + id2string(entry_location.function_name), + "func_init_done", + source_locationt::nil(), + called_function_symbol->mode, + symbol_table); + func_init_done_symbol.is_static_lifetime = true; + func_init_done_symbol.value = false_exprt(); + symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr(); + + add_init_section(func_init_done_var, goto_model); code_blockt harness_function_body = add_assignments_to_globals(snapshot, goto_model); + harness_function_body.add(code_assignt{func_init_done_var, false_exprt{}}); + add_call_with_nondet_arguments( *called_function_symbol, harness_function_body); @@ -350,3 +296,133 @@ void memory_snapshot_harness_generatort::generate( goto_functions.update(); } + +memory_snapshot_harness_generatort::entry_goto_locationt +memory_snapshot_harness_generatort::parse_goto_location( + const std::string &cmdl_option) +{ + std::vector start; + split_string(cmdl_option, ':', start, true); + + if( + start.empty() || start.front().empty() || + (start.size() == 2 && start.back().empty()) || start.size() > 2) + { + throw invalid_command_line_argument_exceptiont( + "invalid initial location specification", "--initial-location"); + } + + if(start.size() == 2) + { + const auto location_number = string2optional_unsigned(start.back()); + CHECK_RETURN(location_number.has_value()); + return entry_goto_locationt{start.front(), *location_number}; + } + else + { + return entry_goto_locationt{start.front()}; + } +} + +memory_snapshot_harness_generatort::entry_source_locationt +memory_snapshot_harness_generatort::parse_source_location( + const std::string &cmdl_option) +{ + std::string initial_file_string; + std::string initial_line_string; + split_string( + cmdl_option, ':', initial_file_string, initial_line_string, true); + + if(initial_file_string.empty() || initial_line_string.empty()) + { + throw invalid_command_line_argument_exceptiont( + "invalid initial location specification", "--initial-file-line"); + } + + const auto line_number = string2optional_unsigned(initial_line_string); + CHECK_RETURN(line_number.has_value()); + return entry_source_locationt{initial_file_string, *line_number}; +} + +memory_snapshot_harness_generatort::entry_locationt +memory_snapshot_harness_generatort::initialize_entry_via_goto( + const entry_goto_locationt &entry_goto_location, + const goto_functionst &goto_functions) +{ + PRECONDITION(!entry_goto_location.function_name.empty()); + const irep_idt &function_name = entry_goto_location.function_name; + + // by function(+location): search for the function then jump to n-th + // location, then check the number + const auto &goto_function = + goto_functions.function_map.find(entry_goto_location.function_name); + if( + goto_function != goto_functions.function_map.end() && + goto_function->second.body_available()) + { + const auto &goto_program = goto_function->second.body; + + const auto corresponding_instruction = + entry_goto_location.find_first_corresponding_instruction( + goto_program.instructions); + + if(corresponding_instruction != goto_program.instructions.end()) + return entry_locationt{function_name, corresponding_instruction}; + } + throw invalid_command_line_argument_exceptiont( + "could not find the specified entry point", "--initial-goto-location"); +} + +memory_snapshot_harness_generatort::entry_locationt +memory_snapshot_harness_generatort::initialize_entry_via_source( + const entry_source_locationt &entry_source_location, + const goto_functionst &goto_functions) +{ + PRECONDITION(!entry_source_location.file_name.empty()); + + // by line: iterate over all instructions until source location match + for(const auto &entry : goto_functions.function_map) + { + const auto &goto_function = entry.second; + // if !body_available() then body.instruction.empty() and that's fine + const auto &goto_program = goto_function.body; + + const auto corresponding_instruction = + entry_source_location.find_first_corresponding_instruction( + goto_program.instructions); + + if(corresponding_instruction != goto_program.instructions.end()) + return entry_locationt{entry.first, corresponding_instruction}; + } + throw invalid_command_line_argument_exceptiont( + "could not find the specified entry point", "--initial-source-location"); +} + +goto_programt::const_targett memory_snapshot_harness_generatort:: + entry_goto_locationt::find_first_corresponding_instruction( + const goto_programt::instructionst &instructions) const +{ + if(!location_number.has_value()) + return instructions.begin(); + + return std::find_if( + instructions.begin(), + instructions.end(), + [this](const goto_programt::instructiont &instruction) { + return *location_number == instruction.location_number; + }); +} + +goto_programt::const_targett memory_snapshot_harness_generatort:: + entry_source_locationt::find_first_corresponding_instruction( + const goto_programt::instructionst &instructions) const +{ + return std::find_if( + instructions.begin(), + instructions.end(), + [this](const goto_programt::instructiont &instruction) { + return instruction.source_location.get_file() == file_name && + safe_string2unsigned(id2string( + instruction.source_location.get_line())) >= line_number; + }); +} diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 1568932d1a6..80181ff0305 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -22,7 +22,8 @@ Author: Daniel Poetzl // clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ "(memory-snapshot):" \ - "(initial-location):" \ + "(initial-goto-location):" \ + "(initial-source-location):" \ "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -31,9 +32,11 @@ Author: Daniel Poetzl "memory snapshot harness generator (--harness-type\n" \ " initialise-from-memory-snapshot)\n\n" \ "--memory-snapshot initialise memory from JSON memory snapshot\n"\ - "--initial-location ]>\n" \ + "--initial-goto-location ]>\n" \ " use given function and location number as " \ "entry\n point\n" \ + "--initial-source-location \n" \ + " use given file and line as entry point\n" \ "--havoc-variables vars initialise variables from vars to\n" \ " non-deterministic values" \ // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP @@ -66,6 +69,103 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort override; protected: + /// User provided goto location: function name and (maybe) location number; + /// the structure wraps this option with a parser + struct entry_goto_locationt + { + irep_idt function_name; + optionalt location_number; + + entry_goto_locationt() = delete; + explicit entry_goto_locationt(irep_idt function_name) + : function_name(function_name) + { + } + explicit entry_goto_locationt( + irep_idt function_name, + unsigned location_number) + : function_name(function_name), location_number(location_number) + { + } + + /// Returns the first \ref goto_programt::instructiont represented by this + /// goto location, i.e. if there is no location number then the first + /// instruction, otherwise the one with the right location number + /// \param instructions: list of instructions to be searched + /// \return iterator to the right instruction (or `end()`) + goto_programt::const_targett find_first_corresponding_instruction( + const goto_programt::instructionst &instructions) const; + }; + + /// Parse a command line option to extract the user specified entry goto + /// location + /// \param cmdl_option: a string of the format `name:number` + /// \return correctly constructed entry goto location + entry_goto_locationt parse_goto_location(const std::string &cmdl_option); + + /// User provided source location: file name and line number; the structure + /// wraps this option with a parser + struct entry_source_locationt + { + irep_idt file_name; + unsigned line_number; + + entry_source_locationt() = delete; + explicit entry_source_locationt(irep_idt file_name, unsigned line_number) + : file_name(file_name), line_number(line_number) + { + } + + /// Returns the first \ref goto_programt::instructiont represented by this + /// source location, i.e. one with the same file name and line number + /// \param instructions: list of instructions to be searched + /// \return iterator to the right instruction (or `end()`) + goto_programt::const_targett find_first_corresponding_instruction( + const goto_programt::instructionst &instructions) const; + }; + + /// Parse a command line option to extract the user specified entry source + /// location + /// \param cmdl_option: a string of the format `name:number` + /// \return correctly constructed entry source location + entry_source_locationt parse_source_location(const std::string &cmdl_option); + + /// Wraps the information needed to identify the entry point. Initializes via + /// either \ref entry_goto_locationt or \ref entry_source_locationt + struct entry_locationt + { + irep_idt function_name; + goto_programt::const_targett start_instruction; + + entry_locationt() = default; + explicit entry_locationt( + irep_idt function_name, + goto_programt::const_targett start_instruction) + : function_name(function_name), start_instruction(start_instruction) + { + } + }; + + /// Find and return the entry instruction (requested by the user as goto + /// location: function name + location number) + /// \param entry_goto_location: user specified goto location + /// \param goto_functions: goto functions to be searched for the entry + /// instruction + /// \return the correctly constructed entry location + entry_locationt initialize_entry_via_goto( + const entry_goto_locationt &entry_goto_location, + const goto_functionst &goto_functions); + + /// Find and return the entry instruction (requested by the user as source + /// location: file name + line number) + /// \param entry_source_location: user specified goto location + /// \param goto_functions: goto functions to be searched for the entry + /// instruction + /// \return the correctly constructed entry location + entry_locationt initialize_entry_via_source( + const entry_source_locationt &entry_source_location, + const goto_functionst &goto_functions); + /// Collect the memory-snapshot specific cmdline options (one at a time) /// \param option: memory-snapshot | initial-location | havoc-variables /// \param values: list of arguments related to a given option @@ -114,8 +214,12 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort /// ..second_part.. /// } /// + /// \param func_init_done_var: symbol expression for the `func_init_done` + /// variable /// \param goto_model: Model where the modification takes place - void add_init_section(goto_modelt &goto_model) const; + void add_init_section( + const symbol_exprt &func_init_done_var, + goto_modelt &goto_model) const; /// For each global symbol in the \p snapshot symbol table either: /// 1) add \ref code_assignt assigning a value from the \p snapshot to the @@ -146,12 +250,15 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort goto_modelt &goto_model, const symbolt &function) const; + /// data to store the command-line options std::string memory_snapshot_file; - - irep_idt entry_function_name; - optionalt location_number; + std::string initial_goto_location_line; + std::string initial_source_location_line; std::unordered_set variables_to_havoc; + /// data to initialize the entry function + entry_locationt entry_location; + message_handlert &message_handler; }; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 7e6abf55afb..432c940c448 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -588,28 +588,6 @@ class goto_programt return t; } - optionalt get_target(const unsigned location_number) const - { - PRECONDITION(!instructions.empty()); - - const unsigned start_location_number = instructions.front().location_number; - - if( - location_number < start_location_number || - location_number > instructions.back().location_number) - { - return nullopt; - } - - auto location_target = - std::next(instructions.begin(), location_number - start_location_number); - - // location numbers are contiguous unless new instructions are inserted - // here we check that nobody inserted any instruction into our function - CHECK_RETURN(location_target->location_number == location_number); - return location_target; - } - template std::list get_successors(Target target) const;