27 #include <unordered_set>
29 typedef std::unordered_set<irep_idt>
linest;
30 typedef std::unordered_map<irep_idt, linest>
filest;
39 for(
const auto &instruction : gf_entry.second.body.instructions)
41 const auto &source_location = instruction.source_location();
43 filest &files = dest[source_location.get_working_directory()];
44 const irep_idt &file = source_location.get_file();
46 if(!file.
empty() && !source_location.is_built_in())
48 files[file].insert(source_location.get_line());
61 for(
auto const &files : eloc_map)
62 for(
auto const &lines : files.second)
63 eloc+=lines.second.size();
65 std::cout <<
"Effective lines of code: " << eloc <<
'\n';
73 for(
auto const &files : eloc_map)
74 for(
auto const &lines : files.second)
77 if(!files.first.empty())
79 std::filesystem::path(
id2string(files.first)).append(file).string();
81 for(
const irep_idt &line : lines.second)
82 std::cout << file <<
':' << line <<
'\n';
89 goto_functionst::function_mapt::const_iterator start=
93 !start->second.body_available())
95 std::cout <<
"No entry point found, path length undefined\n";
99 struct visited_cfg_nodet
103 visited_cfg_nodet():visited(
false)
114 const cfgt::entryt &start_node =
116 const cfgt::entryt &last_node =
120 cfg.shortest_path(start_node, last_node, shortest_path);
121 std::cout <<
"Shortest control-flow path: " << shortest_path.size()
122 <<
" instructions\n";
124 std::size_t n_loops=0, loop_ins=0;
131 i_it->is_backwards_goto() ||
132 i_it == gf_entry.second.body.instructions.begin())
134 const cfgt::entryt &node = cfg.get_node_index(i_it);
136 cfg.shortest_loop(node, loop);
141 loop_ins+=loop.size()-1;
148 std::cout <<
"Loop information: " << n_loops <<
" loops, "
149 << loop_ins <<
" instructions in shortest paths of loop bodies\n";
151 std::size_t n_reachable=0;
152 cfg.visit_reachable(start_node);
153 for(std::size_t i=0; i<cfg.size(); ++i)
156 std::cout <<
"Reachable instructions: " << n_reachable <<
"\n";
165 goto_functionst::function_mapt::const_iterator f_it =
167 const bool has_initialize =
169 std::unordered_set<irep_idt> initialized;
173 for(
const auto &ins : f_it->second.body.instructions)
178 ode.
build(ins.assign_lhs(), ns);
193 const symbolt &symbol = symbol_entry.second;
198 (has_initialize && initialized.find(symbol.
name) == initialized.end()))
204 if(bits.has_value() && bits.value() > 0)
205 total_size += bits.value();
208 std::cout <<
"Total size of global objects: " << total_size <<
" bits\n";
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
typet type
Type of symbol.
irep_idt name
The unique identifier.
std::unordered_set< irep_idt > linest
void count_eloc(const goto_modelt &goto_model)
void print_global_state_size(const goto_modelt &goto_model)
std::unordered_map< irep_idt, filest > working_dirst
static void collect_eloc(const goto_modelt &goto_model, working_dirst &dest)
void print_path_lengths(const goto_modelt &goto_model)
std::unordered_map< irep_idt, linest > filest
void list_eloc(const goto_modelt &goto_model)
Count effective lines of code.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
std::list< path_nodet > patht
API to expression classes for Pointers.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.