cprover
Loading...
Searching...
No Matches
branch.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Branch Instrumentation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "branch.h"
13
14#include <util/cprover_prefix.h>
15#include <util/expr_util.h>
16#include <util/prefix.h>
17
19
20#include "function.h"
21
22void branch(
23 goto_modelt &goto_model,
24 const irep_idt &id)
25{
26 for(auto &gf_entry : goto_model.goto_functions.function_map)
27 {
28 // don't instrument our internal functions
29 if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
30 continue;
31
32 // don't instrument the function to be called,
33 // or otherwise this will be recursive
34 if(gf_entry.first == id)
35 continue;
36
37 // patch in a call to `id' at the branch points
38 goto_programt &body = gf_entry.second.body;
39
41 {
42 // if C goto T is transformed into:
43 //
44 // if !C goto T' i_it
45 // id("taken"); t1
46 // goto T t2
47 // T': id("not-taken"); t3
48 // ...
49
50 if(i_it->is_goto() && !i_it->condition().is_constant())
51 {
52 // negate condition
53 i_it->condition_nonconst() = boolean_negate(i_it->condition());
54
56 i_it,
58 function_to_call(goto_model.symbol_table, id, "taken")));
59
61 t1, goto_programt::make_goto(i_it->get_target(), true_exprt()));
62
64 t2,
66 function_to_call(goto_model.symbol_table, id, "not-taken")));
67 i_it->targets.clear();
68 i_it->targets.push_back(t3);
69 }
70 }
71 }
72}
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition branch.cpp:22
Branch Instrumentation.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
The Boolean constant true.
Definition std_expr.h:3008
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition function.cpp:23
Function Entering and Exiting.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47