cprover
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 <analyses/goto_check.h>
15 
20 #include <goto-programs/mm_io.h>
28 
29 #include <util/bitvector_types.h>
30 #include <util/message.h>
31 #include <util/options.h>
32 
34  goto_modelt &goto_model,
35  const optionst &options,
36  messaget &log)
37 {
38  if(options.get_bool_option("string-abstraction"))
39  string_instrumentation(goto_model);
40 
41  // remove function pointers
42  log.status() << "Removal of function pointers and virtual functions"
43  << messaget::eom;
45  log.get_message_handler(),
46  goto_model,
47  options.get_bool_option("pointer-check"));
48 
49  mm_io(goto_model);
50 
51  // instrument library preconditions
52  instrument_preconditions(goto_model);
53 
54  // do partial inlining
55  if(options.get_bool_option("partial-inline"))
56  {
57  log.status() << "Partial Inlining" << messaget::eom;
58  goto_partial_inline(goto_model, log.get_message_handler());
59  }
60 
61  // remove returns, gcc vectors, complex
62  remove_returns(goto_model);
63  remove_vector(goto_model);
64  remove_complex(goto_model);
65  if(options.get_bool_option("rewrite-union"))
66  rewrite_union(goto_model);
67 
68  // add generic checks
69  log.status() << "Generic Property Instrumentation" << messaget::eom;
70  goto_check(options, goto_model);
71 
72  // checks don't know about adjusted float expressions
73  adjust_float_expressions(goto_model);
74 
75  if(options.get_bool_option("string-abstraction"))
76  {
77  log.status() << "String Abstraction" << messaget::eom;
78  string_abstraction(goto_model, log.get_message_handler());
79  }
80 
81  // recalculate numbers, etc.
82  goto_model.goto_functions.update();
83 
84  // add loop ids
86 
87  return false;
88 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
string_abstraction.h
String Abstraction.
rewrite_union.h
Symbolic Execution.
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
mm_io
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:33
messaget::status
mstreamt & status() const
Definition: message.h:414
goto_partial_inline
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...
Definition: goto_inline.cpp:106
instrument_preconditions.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
options.h
Options.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2338
messaget::eom
static eomt eom
Definition: message.h:297
string_instrumentation.h
String Abstraction.
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
Definition: string_abstraction.cpp:69
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:253
remove_complex.h
Remove the 'complex' data type by compilation into structs.
mm_io.h
Perform Memory-mapped I/O instrumentation.
string_instrumentation
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
Definition: string_instrumentation.cpp:153
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
bitvector_types.h
Pre-defined bitvector types.
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
goto_check.h
Program Transformation.
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
process_goto_program
bool process_goto_program(goto_modelt &goto_model, const optionst &options, messaget &log)
Common processing and simplification of goto_programts.
Definition: process_goto_program.cpp:33
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
remove_returns.h
Replace function returns by assignments to global variables.
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:257
goto_functionst::update
void update()
Definition: goto_functions.h:81
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:79
message.h
adjust_float_expressions.h
Symbolic Execution.
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:524
remove_function_pointers.h
Remove Indirect Function Calls.
process_goto_program.h