cprover
ai_baset Class Referenceabstract

#include <ai.h>

Inheritance diagram for ai_baset:
[legend]
Collaboration diagram for ai_baset:
[legend]

Public Types

typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 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 void clear ()
 
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
 

Protected Types

typedef std::map< unsigned, locationtworking_sett
 
typedef std::set< irep_idtrecursion_sett
 

Protected Member Functions

virtual void initialize (const goto_programt &)
 
virtual void initialize (const goto_functionst::goto_functiont &)
 
virtual void initialize (const goto_functionst &)
 
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)
 
virtual void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)=0
 
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)
 
virtual bool merge (const statet &src, locationt from, locationt to)=0
 
virtual bool merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns)=0
 
virtual statetget_state (locationt l)=0
 
virtual const statetfind_state (locationt l) const =0
 
virtual statetmake_temporary_state (const statet &s)=0
 

Protected Attributes

recursion_sett recursion_set
 

Detailed Description

Definition at line 108 of file ai.h.

Member Typedef Documentation

§ locationt

Definition at line 112 of file ai.h.

§ recursion_sett

typedef std::set<irep_idt> ai_baset::recursion_sett
protected

Definition at line 308 of file ai.h.

§ statet

Definition at line 111 of file ai.h.

§ working_sett

typedef std::map<unsigned, locationt> ai_baset::working_sett
protected

Definition at line 271 of file ai.h.

Constructor & Destructor Documentation

§ ai_baset()

ai_baset::ai_baset ( )
inline

Definition at line 114 of file ai.h.

§ ~ai_baset()

virtual ai_baset::~ai_baset ( )
inlinevirtual

Definition at line 118 of file ai.h.

Member Function Documentation

§ clear()

§ concurrent_fixedpoint()

void ai_baset::concurrent_fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
protected

§ do_function_call()

bool ai_baset::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

Definition at line 379 of file ai.cpp.

§ do_function_call_rec()

bool ai_baset::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 
)
protected

Definition at line 442 of file ai.cpp.

References goto_functions_templatet< bodyT >::function_map, and id2string().

§ entry_state() [1/2]

void ai_baset::entry_state ( const goto_programt goto_program)
protected

§ entry_state() [2/2]

void ai_baset::entry_state ( const goto_functionst goto_functions)
protected

§ find_state()

§ fixedpoint() [1/2]

bool ai_baset::fixedpoint ( const goto_programt goto_program,
const goto_functionst goto_functions,
const namespacet ns 
)
protected

§ fixedpoint() [2/2]

§ get_next()

ai_baset::locationt ai_baset::get_next ( working_sett working_set)
protected

Definition at line 283 of file ai.cpp.

§ get_state()

§ initialize() [1/3]

void ai_baset::initialize ( const goto_programt goto_program)
protectedvirtual

§ initialize() [2/3]

void ai_baset::initialize ( const goto_functionst::goto_functiont goto_function)
protectedvirtual

Definition at line 264 of file ai.cpp.

§ initialize() [3/3]

void ai_baset::initialize ( const goto_functionst goto_functions)
protectedvirtual

§ make_temporary_state()

§ merge()

§ merge_shared()

§ operator()() [1/4]

void ai_baset::operator() ( const goto_programt goto_program,
const namespacet ns 
)
inline

Definition at line 122 of file ai.h.

§ operator()() [2/4]

void ai_baset::operator() ( const goto_functionst goto_functions,
const namespacet ns 
)
inline

Definition at line 132 of file ai.h.

§ operator()() [3/4]

void ai_baset::operator() ( const goto_modelt goto_model)
inline

Definition at line 141 of file ai.h.

References goto_modelt::goto_functions, and goto_modelt::symbol_table.

§ operator()() [4/4]

void ai_baset::operator() ( const goto_functionst::goto_functiont goto_function,
const namespacet ns 
)
inline

Definition at line 149 of file ai.h.

§ output() [1/5]

void ai_baset::output ( const namespacet ns,
const goto_functionst goto_functions,
std::ostream &  out 
) const
virtual

§ output() [2/5]

void ai_baset::output ( const goto_modelt goto_model,
std::ostream &  out 
) const
inline

§ output() [3/5]

void ai_baset::output ( const namespacet ns,
const goto_programt goto_program,
std::ostream &  out 
) const
inline

Definition at line 176 of file ai.h.

References ai_domain_baset::output().

§ output() [4/5]

void ai_baset::output ( const namespacet ns,
const goto_functionst::goto_functiont goto_function,
std::ostream &  out 
) const
inline

Definition at line 184 of file ai.h.

References ai_domain_baset::output(), and ai_domain_baset::output_json().

§ output() [5/5]

void ai_baset::output ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier,
std::ostream &  out 
) const
protectedvirtual

§ output_json() [1/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_functionst goto_functions 
) const
virtual

Output the domains for the whole program as JSON.

parameters: The namespace and goto_functions
Returns
The JSON object

Definition at line 134 of file ai.cpp.

References forall_goto_functions, id2string(), and ai_domain_baset::output_json().

§ output_json() [2/5]

jsont ai_baset::output_json ( const goto_modelt goto_model) const
inline

§ output_json() [3/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_programt goto_program 
) const
inline

Definition at line 204 of file ai.h.

References ai_domain_baset::output_json().

§ output_json() [4/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_functionst::goto_functiont goto_function 
) const
inline

Definition at line 211 of file ai.h.

References ai_domain_baset::output_json(), and ai_domain_baset::output_xml().

§ output_json() [5/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier 
) const
protectedvirtual

Output the domains for a single function as JSON.

parameters: The namespace, goto_program and it's identifier
Returns
The JSON object

Definition at line 159 of file ai.cpp.

References forall_goto_program_instructions, goto_programt::output_instruction(), and json_arrayt::push_back().

§ output_xml() [1/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_functionst goto_functions 
) const
virtual

Output the domains for the whole program as XML.

parameters: The namespace and goto_functions
Returns
The XML object

Definition at line 189 of file ai.cpp.

References forall_goto_functions, id2string(), xmlt::new_element(), ai_domain_baset::output_xml(), and xmlt::set_attribute().

§ output_xml() [2/5]

xmlt ai_baset::output_xml ( const goto_modelt goto_model) const
inline

§ output_xml() [3/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_programt goto_program 
) const
inline

Definition at line 230 of file ai.h.

References ai_domain_baset::output_xml().

§ output_xml() [4/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_functionst::goto_functiont goto_function 
) const
inline

§ output_xml() [5/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier 
) const
protectedvirtual

Output the domains for a single function as XML.

parameters: The namespace, goto_program and it's identifier
Returns
The XML object

Definition at line 217 of file ai.cpp.

References forall_goto_program_instructions, xmlt::new_element(), goto_programt::output_instruction(), ai_domain_baset::output_xml(), and xmlt::set_attribute().

§ put_in_working_set()

void ai_baset::put_in_working_set ( working_sett working_set,
locationt  l 
)
inlineprotected

Definition at line 275 of file ai.h.

§ sequential_fixedpoint()

void ai_baset::sequential_fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
protected

§ visit()

Member Data Documentation

§ recursion_set

recursion_sett ai_baset::recursion_set
protected

Definition at line 309 of file ai.h.


The documentation for this class was generated from the following files: