50 const std::set<irep_idt> &elements)
52 thrown.insert(elements.begin(), elements.end());
56 const std::vector<irep_idt> &elements)
58 thrown.insert(elements.begin(), elements.end());
70 switch(instruction.
type())
81 std::vector<irep_idt> subtypes =
90 if(!instruction.
targets.empty())
98 for(
const auto &
exc : exception_list)
101 std::vector<irep_idt> subtypes=
103 last_caught.insert(subtypes.begin(), subtypes.end());
126 "identifier expected to be a symbol");
130 join(
uea.exceptions_map[function_name]);
155 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
160 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
194 if(goto_program.
empty())
217 (
void)goto_functions;
228 const auto &
fs=found->second;
231 std::cout <<
"Uncaught exceptions in function " <<
232 fn <<
": " << std::endl;
235 std::cout << std::endl;
257 std::map<
irep_idt, std::set<irep_idt>> &exceptions_map)
260 exceptions(goto_functions, ns, exceptions_map);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
idst get_children_trans(const irep_idt &id) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
A collection of goto functions.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
const codet & get_code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool empty() const
Is the program empty?
const irept & find(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...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
computes in exceptions_map an overapproximation of the exceptions thrown by each method
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
uncaught_exceptions_domaint domain
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it.
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
exceptions_mapt exceptions_map
void collect_uncaught_exceptions(const goto_functionst &, const namespacet &)
Runs the uncaught exceptions analysis, which populates the exceptions map.
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
void operator()(const namespacet &ns)
Constructs the class hierarchy.
std::set< irep_idt > thrown
stack_caughtt stack_caught
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
static irep_idt get_exception_type(const pointer_typet &)
Returns the compile type of an exception.
class_hierarchyt class_hierarchy
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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.
Over-approximative uncaught exceptions analysis.