cprover
Loading...
Searching...
No Matches
process_goto_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Process a Goto Program
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7\*******************************************************************/
8
11
13
14#include <analyses/goto_check.h>
15
20#include <goto-programs/mm_io.h>
28
29#include <util/message.h>
30#include <util/options.h>
31
33 goto_modelt &goto_model,
34 const optionst &options,
35 messaget &log)
36{
37 if(options.get_bool_option("string-abstraction"))
38 string_instrumentation(goto_model);
39
40 // remove function pointers
41 log.status() << "Removal of function pointers and virtual functions"
45 goto_model,
46 options.get_bool_option("pointer-check"));
47
48 mm_io(goto_model);
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;
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 // add generic checks
75 log.status() << "Generic Property Instrumentation" << messaget::eom;
76 goto_check(options, goto_model, log.get_message_handler());
77
78 // checks don't know about adjusted float expressions
79 adjust_float_expressions(goto_model);
80
81 if(options.get_bool_option("string-abstraction"))
82 {
83 log.status() << "String Abstraction" << messaget::eom;
84 string_abstraction(goto_model, log.get_message_handler());
85 }
86
87 // recalculate numbers, etc.
88 goto_model.goto_functions.update();
89
90 // add loop ids
92
93 return false;
94}
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.
void compute_loop_numbers()
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
Checks for Errors in C and Java Programs.
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)
void mm_io(const exprt &mm_io_r, const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:37
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.
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)
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.
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(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
String Abstraction.
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
String Abstraction.