cprover
locs.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Locations
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "locs.h"
13 
15  const namespacet &_ns):
16  ns(_ns)
17 {
18 }
19 
20 void locst::build(const goto_functionst &goto_functions)
21 {
22  // build locations
23 
24  typedef std::map<goto_programt::const_targett,
25  loc_reft> target_mapt;
26 
27  target_mapt target_map;
28 
29  forall_goto_functions(f_it, goto_functions)
30  {
31  const goto_functionst::goto_functiont &goto_function = f_it->second;
32 
33  function_entryt &function_entry=function_map[f_it->first];
34  function_entry.type=goto_function.type;
35 
36  if(goto_function.body_available())
37  {
38  const loc_reft entry_loc=end();
39  function_entry.first_loc=entry_loc;
40 
41  forall_goto_program_instructions(i_it, goto_function.body)
42  {
43  target_map[i_it]=end();
44  loc_vector.push_back(loct(i_it, f_it->first));
45  }
46  }
47  else
48  function_entry.first_loc=loc_reft::nil();
49  }
50 
52  function_map.end())
53  throw "no entry point";
54 
56 
57  // build branch targets
58  for(unsigned l=0; l<loc_vector.size(); l++)
59  {
60  const goto_programt::instructiont &i=*loc_vector[l].target;
61 
62  if(i.targets.empty())
63  {
64  }
65  else if(i.targets.size()==1)
66  {
67  const target_mapt::const_iterator m_it=target_map.find(i.get_target());
68 
69  if(m_it==target_map.end())
70  throw "locst::build: jump target not found";
71 
72  const loc_reft target=m_it->second;
73 
74  if(target.loc_number>=loc_vector.size())
75  throw "locst::build: illegal jump target";
76 
77  loc_vector[l].branch_target=target;
78  }
79  else
80  throw "locst does not support more than one branch target";
81  }
82 }
83 
84 void locst::output(std::ostream &out) const
85 {
86  irep_idt function;
87 
88  for(unsigned l=0; l<loc_vector.size(); l++)
89  {
90  const loct &loc=loc_vector[l];
91  if(function!=loc.function)
92  {
93  function=loc.function;
94  out << "*** " << function << "\n";
95  }
96 
97  out << " L" << l << ": "
98 // << loc.target->type << " "
99 // << loc.target->location
100  << " " << as_string(ns, *loc.target) << "\n";
101 
102  if(!loc.branch_target.is_nil())
103  out << " T: " << loc.branch_target << "\n";
104  }
105 
106  out << "\n";
107  out << "The entry location is L" << entry_loc << ".\n";
108 }
#define loc()
loc_reft entry_loc
Definition: locs.h:44
code_typet type
Definition: locs.h:50
unsigned loc_number
Definition: loc_ref.h:20
const namespacet & ns
Definition: locs.h:92
void output(std::ostream &out) const
Definition: locs.cpp:84
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
locst(const namespacet &_ns)
Definition: locs.cpp:14
instructionst::const_iterator const_targett
TO_BE_DOCUMENTED.
Definition: namespace.h:62
loc_vectort loc_vector
Definition: locs.h:43
static loc_reft nil()
Definition: loc_ref.h:48
Definition: locs.h:21
function_mapt function_map
Definition: locs.h:54
CFG made of Program Locations, built from goto_functionst.
loc_reft first_loc
Definition: locs.h:49
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
loc_reft end() const
Definition: locs.h:79
void build(const goto_functionst &goto_functions)
Definition: locs.cpp:20