CBMC
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 
18 
19 #include "function.h"
20 
21 void branch(
22  goto_modelt &goto_model,
23  const irep_idt &id)
24 {
25  for(auto &gf_entry : goto_model.goto_functions.function_map)
26  {
27  // don't instrument our internal functions
28  if(gf_entry.first.starts_with(CPROVER_PREFIX))
29  continue;
30 
31  // don't instrument the function to be called,
32  // or otherwise this will be recursive
33  if(gf_entry.first == id)
34  continue;
35 
36  // patch in a call to `id' at the branch points
37  goto_programt &body = gf_entry.second.body;
38 
40  {
41  // if C goto T is transformed into:
42  //
43  // if !C goto T' i_it
44  // id("taken"); t1
45  // goto T t2
46  // T': id("not-taken"); t3
47  // ...
48 
49  if(i_it->is_goto() && !i_it->condition().is_constant())
50  {
51  // negate condition
52  i_it->condition_nonconst() = boolean_negate(i_it->condition());
53 
55  i_it,
57  function_to_call(goto_model.symbol_table, id, "taken")));
58 
60  t1, goto_programt::make_goto(i_it->get_target(), true_exprt()));
61 
63  t2,
65  function_to_call(goto_model.symbol_table, id, "not-taken")));
66  i_it->targets.clear();
67  i_it->targets.push_back(t3);
68  }
69  }
70  }
71 }
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:21
Branch Instrumentation.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:708
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:3055
#define CPROVER_PREFIX
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:129
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:22
Function Entering and Exiting.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)