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

◆ 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

◆ 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 do_function_call(), goto_functions_templatet< bodyT >::function_map, id2string(), and recursion_set.

Referenced by visit().

◆ entry_state() [1/2]

void ai_baset::entry_state ( const goto_programt goto_program)
protected

Definition at line 258 of file ai.cpp.

References get_state(), and goto_program_templatet< codeT, guardT >::instructions.

Referenced by entry_state(), and operator()().

◆ 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.

Referenced by concurrent_fixedpoint(), and fixedpoint().

◆ get_state()

◆ initialize() [1/3]

◆ initialize() [2/3]

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

Definition at line 264 of file ai.cpp.

References initialize().

◆ 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.

References entry_state(), fixedpoint(), and initialize().

Referenced by constant_propagator_ait::constant_propagator_ait().

◆ operator()() [2/4]

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

Definition at line 132 of file ai.h.

References entry_state(), fixedpoint(), and initialize().

◆ operator()() [3/4]

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

◆ 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.

References entry_state(), fixedpoint(), and initialize().

◆ 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

Definition at line 168 of file ai.h.

References goto_modelt::goto_functions, output(), and goto_modelt::symbol_table.

◆ 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 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 output().

◆ 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, and id2string().

Referenced by output_json().

◆ output_json() [2/5]

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

Definition at line 197 of file ai.h.

References goto_modelt::goto_functions, output_json(), and goto_modelt::symbol_table.

◆ 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 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 output_json().

◆ 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 find_state(), forall_goto_program_instructions, goto_programt::output_instruction(), ai_domain_baset::output_json(), 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(), and xmlt::set_attribute().

Referenced by output_xml().

◆ output_xml() [2/5]

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

Definition at line 223 of file ai.h.

References goto_modelt::goto_functions, output_xml(), and goto_modelt::symbol_table.

◆ 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 output_xml().

◆ output_xml() [4/5]

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

Definition at line 237 of file ai.h.

References output_xml().

◆ 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 find_state(), forall_goto_program_instructions, xmlt::new_element(), goto_programt::output_instruction(), 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.

Referenced by concurrent_fixedpoint(), fixedpoint(), and visit().

◆ 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.

Referenced by do_function_call_rec().


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