Go to the documentation of this file.
17 #include <unordered_set>
28 typedef std::unordered_set<irep_idt>
linest;
29 typedef std::unordered_map<irep_idt, linest>
filest;
40 filest &files=dest[it->source_location.get_working_directory()];
44 !it->source_location.is_built_in())
45 files[
file].insert(it->source_location.get_line());
57 for(
auto const &files : eloc_map)
58 for(
auto const &lines : files.second)
59 eloc+=lines.second.size();
61 std::cout <<
"Effective lines of code: " << eloc <<
'\n';
69 for(
auto const &files : eloc_map)
70 for(
auto const &lines : files.second)
73 if(!files.first.empty())
76 for(
const irep_idt &line : lines.second)
77 std::cout <<
file <<
':' << line <<
'\n';
84 goto_functionst::function_mapt::const_iterator start=
88 !start->second.body_available())
90 std::cout <<
"No entry point found, path length undefined\n";
94 struct visited_cfg_nodet
98 visited_cfg_nodet():visited(
false)
109 const cfgt::entryt &start_node =
111 const cfgt::entryt &last_node =
115 cfg.shortest_path(start_node, last_node, shortest_path);
116 std::cout <<
"Shortest control-flow path: " << shortest_path.size()
117 <<
" instructions\n";
119 std::size_t n_loops=0, loop_ins=0;
123 if(i_it->is_backwards_goto() ||
124 i_it==gf_it->second.body.instructions.begin())
126 const cfgt::entryt &node = cfg.get_node_index(i_it);
128 cfg.shortest_loop(node, loop);
133 loop_ins+=loop.size()-1;
138 std::cout <<
"Loop information: " << n_loops <<
" loops, "
139 << loop_ins <<
" instructions in shortest paths of loop bodies\n";
141 std::size_t n_reachable=0;
142 cfg.visit_reachable(start_node);
143 for(std::size_t i=0; i<cfg.size(); ++i)
146 std::cout <<
"Reachable instructions: " << n_reachable <<
"\n";
155 goto_functionst::function_mapt::const_iterator f_it =
157 const bool has_initialize =
159 std::unordered_set<irep_idt> initialized;
163 for(
const auto &ins : f_it->second.body.instructions)
184 const symbolt &symbol = symbol_entry.second;
189 (has_initialize && initialized.find(symbol.
name) == initialized.end()))
195 if(bits.has_value() && bits.value() > 0)
196 total_size += bits.value();
199 std::cout <<
"Total size of global objects: " << total_size <<
" bits\n";
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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...
void print_global_state_size(const goto_modelt &goto_model)
std::unordered_map< irep_idt, linest > filest
typet type
Type of symbol.
Split an expression into a base object and a (byte) offset.
Count effective lines of code.
function_mapt function_map
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool get_bool(const irep_namet &name) const
const std::string & id2string(const irep_idt &d)
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
const irep_idt & get_identifier() const
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.
void count_eloc(const goto_modelt &goto_model)
const irep_idt & id() const
const exprt & root_object() const
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
instructionst instructions
The list of instructions in the goto program.
goto_functionst goto_functions
GOTO functions.
std::list< path_nodet > patht
const symbolst & symbols
Read-only field, used to look up symbols given their names.
std::unordered_map< irep_idt, filest > working_dirst
A generic container class for the GOTO intermediate representation of one function.
#define forall_goto_functions(it, functions)
bool has_prefix(const std::string &s, const std::string &prefix)
std::unordered_set< irep_idt > linest
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A codet representing an assignment in the program.
void list_eloc(const goto_modelt &goto_model)
static void collect_eloc(const goto_modelt &goto_model, working_dirst &dest)
symbol_tablet symbol_table
Symbol table.
void print_path_lengths(const goto_modelt &goto_model)
irep_idt name
The unique identifier.
#define forall_goto_program_instructions(it, program)