cprover
|
#include <custom_bitvector_analysis.h>
Public Types | |
typedef numbering< irep_idt > | bitst |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef ai_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
void | instrument (goto_functionst &) |
void | check (const goto_modelt &, bool xml, std::ostream &) |
exprt | eval (const exprt &src, locationt loc) |
unsigned | get_bit_nr (const exprt &) |
![]() | |
ait () | |
custom_bitvector_domaint & | operator[] (locationt l) |
const custom_bitvector_domaint & | operator[] (locationt l) const |
const ai_domain_baset & | abstract_state_before (goto_programt::const_targett t) const override |
Returns the abstract state before the given instruction. More... | |
void | clear () override |
![]() | |
ai_baset () | |
virtual | ~ai_baset () |
void | operator() (const goto_programt &goto_program, const namespacet &ns) |
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
void | operator() (const goto_modelt &goto_model) |
void | operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
virtual const ai_domain_baset & | abstract_state_after (goto_programt::const_targett t) const |
Returns the abstract state after the given instruction. More... | |
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
void | output (const goto_modelt &goto_model, std::ostream &out) const |
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as JSON. More... | |
jsont | output_json (const goto_modelt &goto_model) const |
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
Output the domains for the whole program as XML. More... | |
xmlt | output_xml (const goto_modelt &goto_model) const |
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
Public Attributes | |
bitst | bits |
Protected Member Functions | |
virtual void | initialize (const goto_functionst &_goto_functions) |
std::set< exprt > | aliases (const exprt &, locationt loc) |
![]() | |
virtual statet & | get_state (locationt l) override |
const statet & | find_state (locationt l) const override |
bool | merge (const statet &src, locationt from, locationt to) override |
std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
![]() | |
virtual void | initialize (const goto_programt &) |
virtual void | initialize (const goto_functionst::goto_functiont &) |
virtual void | finalize () |
void | entry_state (const goto_programt &) |
void | entry_state (const goto_functionst &) |
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as JSON. More... | |
virtual xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
Output the domains for a single function as XML. More... | |
locationt | get_next (working_sett &working_set) |
void | put_in_working_set (working_sett &working_set, locationt l) |
bool | fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns) |
bool | do_function_call (locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns) |
Protected Attributes | |
local_may_alias_factoryt | local_may_alias_factory |
![]() | |
state_mapt | state_map |
Friends | |
class | custom_bitvector_domaint |
Additional Inherited Members | |
![]() | |
typedef std::unordered_map< locationt, custom_bitvector_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
![]() | |
typedef std::map< unsigned, locationt > | working_sett |
Definition at line 147 of file custom_bitvector_analysis.h.
Definition at line 162 of file custom_bitvector_analysis.h.
|
protected |
Definition at line 192 of file custom_bitvector_analysis.cpp.
References local_may_alias_factoryt::get(), irept::id(), loc, local_may_alias_factory, dereference_exprt::pointer(), to_dereference_expr(), to_typecast_expr(), and exprt::type().
Referenced by custom_bitvector_domaint::assign_struct_rec(), and custom_bitvector_domaint::transform().
void custom_bitvector_analysist::check | ( | const goto_modelt & | goto_model, |
bool | xml, | ||
std::ostream & | out | ||
) |
Definition at line 750 of file custom_bitvector_analysis.cpp.
References dstringt::empty(), eval(), forall_goto_functions, forall_goto_program_instructions, from_expr(), goto_modelt::goto_functions, custom_bitvector_domaint::has_get_must_or_may(), exprt::is_false(), exprt::is_true(), simplify_expr(), goto_modelt::symbol_table, and xml().
Referenced by goto_instrument_parse_optionst::doit().
Definition at line 155 of file custom_bitvector_analysis.h.
References custom_bitvector_domaint::eval(), loc, and ait< custom_bitvector_domaint >::operator[]().
Referenced by check(), and taint_analysist::operator()().
unsigned custom_bitvector_analysist::get_bit_nr | ( | const exprt & | string_expr | ) |
Definition at line 174 of file custom_bitvector_analysis.cpp.
References index_exprt::array(), bits, irept::get(), irept::id(), template_numberingt< Map >::number(), address_of_exprt::object(), unary_exprt::op(), to_address_of_expr(), to_index_expr(), and to_typecast_expr().
Referenced by custom_bitvector_domaint::eval(), and custom_bitvector_domaint::transform().
|
inlineprotectedvirtual |
Reimplemented from ai_baset.
Definition at line 166 of file custom_bitvector_analysis.h.
References ai_baset::initialize(), and local_may_alias_factory.
void custom_bitvector_analysist::instrument | ( | goto_functionst & | ) |
Definition at line 746 of file custom_bitvector_analysis.cpp.
|
friend |
Definition at line 172 of file custom_bitvector_analysis.h.
bitst custom_bitvector_analysist::bits |
Definition at line 163 of file custom_bitvector_analysis.h.
Referenced by get_bit_nr(), and custom_bitvector_domaint::output().
|
protected |
Definition at line 174 of file custom_bitvector_analysis.h.
Referenced by aliases(), and initialize().