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/prefix.h>
16 
17 #include "function.h"
18 
19 void branch(
20  goto_modelt &goto_model,
21  const irep_idt &id)
22 {
23  Forall_goto_functions(f_it, goto_model.goto_functions)
24  {
25  // don't instrument our internal functions
26  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
27  continue;
28 
29  // don't instrument the function to be called,
30  // or otherwise this will be recursive
31  if(f_it->first==id)
32  continue;
33 
34  // patch in a call to `id' at the branch points
35  goto_programt &body=f_it->second.body;
36 
38  {
39  // if C goto T is transformed into:
40  //
41  // if !C goto T' i_it
42  // id("taken"); t1
43  // goto T t2
44  // T': id("not-taken"); t3
45  // ...
46 
47  if(i_it->is_goto() &&
48  !i_it->guard.is_constant())
49  {
50  // negate condition
51  i_it->guard.make_not();
52 
54  t1->make_function_call(
55  function_to_call(goto_model.symbol_table, id, "taken"));
56  t1->function=f_it->first;
57 
59  t2->make_goto(i_it->get_target());
60 
62  t3->make_function_call(
63  function_to_call(goto_model.symbol_table, id, "not-taken"));
64  t3->function=f_it->first;
65  i_it->targets.clear();
66  i_it->targets.push_back(t3);
67  }
68  }
69  }
70 }
Function Entering and Exiting.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
#define CPROVER_PREFIX
Branch Instrumentation.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
instructionst::iterator targett
Definition: goto_program.h:397
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:21
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:19