Go to the documentation of this file.
31 if(expr.
id() != ID_symbol && expr.
operands().size() >= 1)
45 const std::set<irep_idt> &elements)
47 thrown.insert(elements.begin(), elements.end());
51 const std::vector<irep_idt> &elements)
53 thrown.insert(elements.begin(), elements.end());
65 switch(instruction.
type)
75 std::vector<irep_idt> subtypes =
84 if(!instruction.
targets.empty())
86 std::set<irep_idt> caught;
92 for(
const auto &exc : exception_list)
94 last_caught.insert(exc.id());
95 std::vector<irep_idt> subtypes=
97 last_caught.insert(subtypes.begin(), subtypes.end());
107 for(
const auto &exc_id : caught)
117 const exprt &function_expr=
120 function_expr.
id()==ID_symbol,
121 "identifier expected to be a symbol");
150 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
155 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
187 const goto_programt &goto_program=current_function->second.body;
189 if(goto_program.
empty())
198 if(
exceptions_map[current_function->first].size()<elements.size())
212 (void)goto_functions;
216 const auto fn=it->first;
217 const exceptions_mapt::const_iterator found=
exceptions_map.find(fn);
223 const auto &fs=found->second;
226 std::cout <<
"Uncaught exceptions in function " <<
227 fn <<
": " << std::endl;
228 for(
const auto exc_id : fs)
230 std::cout << std::endl;
252 std::map<
irep_idt, std::set<irep_idt>> &exceptions_map)
255 exceptions(goto_functions, ns, exceptions_map);
const irep_idt & get_identifier() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
The type of an expression, extends irept.
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it.
goto_program_instruction_typet type
What kind of instruction?
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
const irept & find(const irep_namet &name) const
bool empty() const
Is the program empty?
Base class for all expressions.
targetst targets
The list of successor instructions.
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
void collect_uncaught_exceptions(const goto_functionst &, const namespacet &)
Runs the uncaught exceptions analysis, which populates the exceptions map.
std::set< irep_idt > thrown
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool has_operands() const
Return true if there is at least one operand.
const std::string & id2string(const irep_idt &d)
stack_caughtt stack_caught
codet code
Do not read or modify directly – use get_X() instead.
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const code_function_callt & to_code_function_call(const codet &code)
class_hierarchyt class_hierarchy
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
uncaught_exceptions_domaint domain
A collection of goto functions.
void uncaught_exceptions(const goto_functionst &goto_functions, const namespacet &ns, std::map< irep_idt, std::set< irep_idt >> &exceptions_map)
Applies the uncaught exceptions analysis and outputs the result.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
exceptions_mapt exceptions_map
void operator()(const namespacet &ns)
Constructs the class hierarchy.
Over-approximative uncaught exceptions analysis.
A generic container class for the GOTO intermediate representation of one function.
computes in exceptions_map an overapproximation of the exceptions thrown by each method
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
This class represents an instruction in the GOTO intermediate representation.
#define forall_goto_program_instructions(it, program)
idst get_children_trans(const irep_idt &id) const