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