46 const std::set<irep_idt> &elements)
48 thrown.insert(elements.begin(), elements.end());
52 const std::vector<irep_idt> &elements)
54 thrown.insert(elements.begin(), elements.end());
66 switch(instruction.
type)
76 std::vector<irep_idt> subtypes =
85 if(!instruction.
targets.empty())
87 std::set<irep_idt> caught;
93 for(
const auto &exc : exception_list)
95 last_caught.insert(exc.id());
96 std::vector<irep_idt> subtypes=
98 last_caught.insert(subtypes.begin(), subtypes.end());
108 for(
const auto &exc_id : caught)
118 const exprt &function_expr=
121 function_expr.
id()==ID_symbol,
122 "identifier expected to be a symbol");
172 if(
exceptions_map[current_function->first].size()<elements.size())
189 const auto fn=it->first;
190 const exceptions_mapt::const_iterator found=
exceptions_map.find(fn);
196 const auto &fs=found->second;
199 std::cout <<
"Uncaught exceptions in function " <<
200 fn <<
": " << std::endl;
201 for(
const auto exc_id : fs)
203 std::cout << std::endl;
225 std::map<
irep_idt, std::set<irep_idt>> &exceptions_map)
228 exceptions(goto_functions, ns, exceptions_map);
The type of an expression.
const std::string & id2string(const irep_idt &d)
Over-approximative uncaught exceptions analysis.
exceptions_mapt exceptions_map
const symbol_tablet & get_symbol_table() const
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it...
std::vector< irept > subt
goto_program_instruction_typet type
What kind of instruction?
const irep_idt & get_identifier() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
targetst targets
The list of successor instructions.
std::set< irep_idt > thrown
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
This class represents an instruction in the GOTO intermediate representation.
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
const irep_idt & id() const
stack_caughtt stack_caught
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.
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
instructionst::const_iterator const_targett
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
class_hierarchyt class_hierarchy
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.
bool has_operands() const
void operator()(const namespacet &ns)
Constructs the class hierarchy.
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
A generic container class for the GOTO intermediate representation of one function.
Base class for all expressions.
bool empty() const
Is the program empty?
goto_programt & goto_program
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
#define forall_goto_functions(it, functions)
idst get_children_trans(const irep_idt &id) const
uncaught_exceptions_domaint domain
#define forall_goto_program_instructions(it, program)
computes in exceptions_map an overapproximation of the exceptions thrown by each method ...
const irept & find(const irep_namet &name) const
const code_function_callt & to_code_function_call(const codet &code)