17#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();
46 if(!
file.empty() && !source_location.is_built_in())
48 files[
file].insert(source_location.get_line());
62 for(
auto const &lines :
files.second)
63 eloc+=lines.second.size();
65 std::cout <<
"Effective lines of code: " <<
eloc <<
'\n';
74 for(
auto const &lines :
files.second)
77 if(!
files.first.empty())
80 for(
const irep_idt &line : lines.second)
81 std::cout <<
file <<
':' << line <<
'\n';
88 goto_functionst::function_mapt::const_iterator
start=
92 !
start->second.body_available())
94 std::cout <<
"No entry point found, path length undefined\n";
118 cfgt::patht shortest_path;
120 std::cout <<
"Shortest control-flow path: " << shortest_path.size()
121 <<
" instructions\n";
130 i_it->is_backwards_goto() ||
133 const cfgt::entryt &node = cfg.get_node_index(
i_it);
135 cfg.shortest_loop(node, loop);
147 std::cout <<
"Loop information: " <<
n_loops <<
" loops, "
148 <<
loop_ins <<
" instructions in shortest paths of loop bodies\n";
152 for(std::size_t
i=0;
i<cfg.size(); ++
i)
155 std::cout <<
"Reachable instructions: " <<
n_reachable <<
"\n";
164 goto_functionst::function_mapt::const_iterator
f_it =
168 std::unordered_set<irep_idt> initialized;
172 for(
const auto &
ins :
f_it->second.body.instructions)
177 ode.build(
ins.assign_lhs(), ns);
203 if(bits.has_value() && bits.value() > 0)
207 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.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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.
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
optionalt< 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.