27#include <unordered_set>
29typedef std::unordered_set<irep_idt>
linest;
30typedef 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());
65 std::cout <<
"Effective lines of code: " <<
eloc <<
'\n';
77 if(!
files.first.empty())
79 std::filesystem::path(
id2string(
files.first)).append(file).string();
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";
119 cfgt::patht shortest_path;
121 std::cout <<
"Shortest control-flow path: " << shortest_path.size()
122 <<
" instructions\n";
131 i_it->is_backwards_goto() ||
134 const cfgt::entryt &node = cfg.get_node_index(
i_it);
136 cfg.shortest_loop(node, loop);
148 std::cout <<
"Loop information: " <<
n_loops <<
" loops, "
149 <<
loop_ins <<
" instructions in shortest paths of loop bodies\n";
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 =
169 std::unordered_set<irep_idt> initialized;
173 for(
const auto &
ins :
f_it->second.body.instructions)
178 ode.build(
ins.assign_lhs(), ns);
204 if(bits.has_value() && bits.value() > 0)
208 std::cout <<
"Total size of global objects: " <<
total_size <<
" bits\n";
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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.
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)
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.