From b7cf102aec9afd4d257eaf4eb6ab75d906a383ac Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 15 Sep 2018 10:12:57 +0100 Subject: [PATCH 1/2] add documentation to read_goto_binary and read_object_and_link --- src/goto-programs/read_goto_binary.cpp | 27 ++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index bc28f789493..d4333852dc6 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -27,6 +27,12 @@ Module: Read Goto Programs #include "elf_reader.h" #include "osx_fat_reader.h" +/// \brief Read a goto binary from a file, but do not update \ref config +/// \param filename the file name of the goto binary +/// \param dest the goto model returned +/// \param message_handler for diagnostics +/// \deprecated Use read_goto_binary(file, message_handler) instead +/// \return true on failure, false on success bool read_goto_binary( const std::string &filename, goto_modelt &dest, @@ -36,6 +42,10 @@ bool read_goto_binary( filename, dest.symbol_table, dest.goto_functions, message_handler); } +/// \brief Read a goto binary from a file, but do not update \ref config +/// \param filename the file name of the goto binary +/// \param message_handler for diagnostics +/// \return goto model on success, {} on failure optionalt read_goto_binary(const std::string &filename, message_handlert &message_handler) { @@ -50,6 +60,12 @@ read_goto_binary(const std::string &filename, message_handlert &message_handler) return std::move(dest); } +/// \brief Read a goto binary from a file, but do not update \ref config +/// \param filename the file name of the goto binary +/// \param symbol_table the symbol table from the goto binary +/// \param goto_functions the goto functions from the goto binary +/// \param message_handler for diagnostics +/// \return true on failure, false on success bool read_goto_binary( const std::string &filename, symbol_tablet &symbol_table, @@ -206,8 +222,10 @@ bool is_goto_binary(const std::string &filename) return false; } -/// reads an object file -/// \par parameters: a file_name +/// \brief reads an object file, and also updates config +/// \param file_name file name of the goto binary +/// \param dest the goto model returned +/// \param message_handler for diagnostics /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, @@ -241,8 +259,9 @@ bool read_object_and_link( return false; } -/// reads an object file -/// \par parameters: a file_name +/// \brief reads an object file, and also updates the config +/// \param file_name file name of the goto binary +/// \param message_handler for diagnostics /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, From 637afdc01d0e6fed3b730c935524499e7c4e9eeb Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 15 Sep 2018 10:13:12 +0100 Subject: [PATCH 2/2] read_goto_binary does not set the config Fixes #2949 This enables auto-detecting the architecture of a goto-binary when performing transformations on it, e.g., with main.c: int main(){ char buffer[] = "a"; int x = strlen(buffer); return x; } the commands goto-cc -m32 -o main.gb main.c goto-instrument --add-library main.gb main2.gb now pass. --- src/goto-instrument/goto_instrument_parse_options.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d7cadc121f1..8a1a8b7e938 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -897,6 +897,8 @@ void goto_instrument_parse_optionst::get_goto_program() { status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom; + config.set(cmdline); + auto result = read_goto_binary(cmdline.args[0], get_message_handler()); if(!result.has_value()) @@ -904,7 +906,7 @@ void goto_instrument_parse_optionst::get_goto_program() goto_model = std::move(result.value()); - config.set(cmdline); + config.set_from_symbol_table(goto_model.symbol_table); } void goto_instrument_parse_optionst::instrument_goto_program()