CBMC
process_goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Process a Goto Program
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "process_goto_program.h"
13 
14 #include <util/message.h>
15 #include <util/options.h>
16 
21 #include <goto-programs/mm_io.h>
29 
32 
33 #include "goto_check.h"
34 
36  goto_modelt &goto_model,
37  const optionst &options,
38  messaget &log)
39 {
40  if(options.get_bool_option("string-abstraction"))
41  string_instrumentation(goto_model);
42 
43  // remove function pointers
44  log.status() << "Removal of function pointers and virtual functions"
45  << messaget::eom;
46  remove_function_pointers(log.get_message_handler(), goto_model, false);
47 
48  mm_io(goto_model, log.get_message_handler());
49 
50  // instrument library preconditions
51  instrument_preconditions(goto_model);
52 
53  // do partial inlining
54  if(options.get_bool_option("partial-inline"))
55  {
56  log.status() << "Partial Inlining" << messaget::eom;
57  goto_partial_inline(goto_model, log.get_message_handler());
58  }
59 
60  // remove returns, gcc vectors, complex
61  if(
62  options.get_bool_option("remove-returns") ||
63  options.get_bool_option("string-abstraction"))
64  {
65  remove_returns(goto_model);
66  }
67 
68  remove_vector(goto_model);
69  remove_complex(goto_model);
70 
71  if(options.get_bool_option("rewrite-union"))
72  rewrite_union(goto_model);
73 
74  if(options.get_bool_option("rewrite-rw-ok"))
75  rewrite_rw_ok(goto_model);
76 
77  // add generic checks
78  log.status() << "Generic Property Instrumentation" << messaget::eom;
79  goto_check_c(options, goto_model, log.get_message_handler());
80  transform_assertions_assumptions(options, goto_model);
81 
82  // checks don't know about adjusted float expressions
83  adjust_float_expressions(goto_model);
84 
85  if(options.get_bool_option("string-abstraction"))
86  {
87  log.status() << "String Abstraction" << messaget::eom;
88  string_abstraction(goto_model, log.get_message_handler());
89  }
90 
91  // recalculate numbers, etc.
92  goto_model.goto_functions.update();
93 
94  return false;
95 }
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static eomt eom
Definition: message.h:289
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Definition: goto_check.cpp:19
Checks for Errors in C and Java Programs.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Program Transformation.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Symbol Table + CFG.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
double log(double x)
Definition: math.c:2776
void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
Definition: mm_io.cpp:154
Perform Memory-mapped I/O instrumentation.
Options.
bool process_goto_program(goto_modelt &goto_model, const optionst &options, messaget &log)
Common processing and simplification of goto_programts.
static void remove_complex(typet &)
removes complex data type
Remove the 'complex' data type by compilation into structs.
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Remove Indirect Function Calls.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
static void remove_vector(typet &)
removes vector data type
Remove the 'vector' data type by compilation into arrays.
static std::optional< exprt > rewrite_rw_ok(exprt expr, const namespacet &ns)
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Symbolic Execution.
void string_abstraction(goto_modelt &goto_model, message_handlert &message_handler)
String Abstraction.
void string_instrumentation(symbol_table_baset &symbol_table, goto_programt &dest)
String Abstraction.