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");
189 if(goto_program.
empty())
212 (void)goto_functions;
216 const auto fn = gf_entry.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);
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.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
goto_program_instruction_typet type
What kind of instruction?
targetst targets
The list of successor instructions.
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_namet &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.
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
The type of an expression, extends irept.
const typet & subtype() 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
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
class_hierarchyt class_hierarchy
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const code_function_callt & to_code_function_call(const codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_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.