Skip to content

Commit ba56cbf

Browse files
author
martin
committed
Add string abstraction to goto-analyzer and goto-diff
At the moment this code is dead and is only added to make the process_goto_program steps more similar. I will leave it to others to decide if this is a useful thing to have and add the required command line options and tests. Should not affect the behaviour of either tool.
1 parent 8296041 commit ba56cbf

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,8 @@ Author: Daniel Kroening, [email protected]
4242
#include <goto-programs/set_properties.h>
4343
#include <goto-programs/show_properties.h>
4444
#include <goto-programs/show_symbol_table.h>
45+
#include <goto-programs/string_abstraction.h>
46+
#include <goto-programs/string_instrumentation.h>
4547
#include <goto-programs/validate_goto_model.h>
4648

4749
#include <analyses/call_stack_history.h>
@@ -884,6 +886,9 @@ bool goto_analyzer_parse_optionst::process_goto_program(
884886

885887
add_malloc_may_fail_variable_initializations(goto_model);
886888

889+
if(options.get_bool_option("string-abstraction"))
890+
string_instrumentation(goto_model);
891+
887892
// remove function pointers
888893
log.status() << "Removing function pointers and virtual functions"
889894
<< messaget::eom;

src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -333,6 +333,9 @@ bool goto_diff_parse_optionst::process_goto_program(
333333

334334
add_malloc_may_fail_variable_initializations(goto_model);
335335

336+
if(options.get_bool_option("string-abstraction"))
337+
string_instrumentation(goto_model);
338+
336339
// remove function pointers
337340
log.status() << "Removal of function pointers and virtual functions"
338341
<< messaget::eom;

0 commit comments

Comments
 (0)