CBMC: Member List

abstract_state_after(locationt l) const ai_baset inlinevirtual

abstract_state_after(const trace_ptrt &p) const ai_baset inlinevirtual

abstract_state_before(locationt l) const ai_baset inlinevirtual

abstract_state_before(const trace_ptrt &p) const ai_baset inlinevirtual

abstract_traces_after(locationt l) const ai_baset inlinevirtual

abstract_traces_before(locationt l) const ai_baset inlinevirtual

ai_baset(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) ai_baset inline

ai_recursive_interproceduralt(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) ai_recursive_interproceduralt inline

ait() ait< domainT > inline

ait(std::unique_ptr< ai_domain_factory_baset > &&df) ait< domainT > inlineexplicit

clear() ai_baset inlinevirtual

cstate_ptrt typedef ai_baset

ctrace_set_ptrt typedef ai_baset

domain_factory ai_baset protected

dummy(const domainT &s) ait< domainT > inlineprivate

entry_state(const goto_programt &goto_program) ai_baset protected

entry_state(const goto_functionst &goto_functions) ai_baset protected

finalize() ai_baset protectedvirtual

fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) ai_baset protectedvirtual

fixedpoint(trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns) ai_baset protectedvirtual

get_next(working_sett &working_set) ai_baset protected

get_state(locationt l) ait< domainT > inlineprotectedvirtual

get_state(trace_ptrt p) ait< domainT > inlineprotectedvirtual

history_factory ai_baset protected

initialize(const irep_idt &function_id, const goto_programt &goto_program) ai_baset protectedvirtual

initialize(const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) ai_baset protectedvirtual

initialize(const goto_functionst &goto_functions) ai_baset protectedvirtual

locationt typedef ait< domainT >

make_temporary_state(const statet &s) ai_baset inlineprotectedvirtual

merge(const statet &src, trace_ptrt from, trace_ptrt to) ai_baset inlineprotectedvirtual

message_handler ai_baset protected

no_logging ait< domainT > private

operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns) ai_baset inline

operator()(const goto_functionst &goto_functions, const namespacet &ns) ai_baset inline

operator()(const abstract_goto_modelt &goto_model) ai_baset inline

operator()(const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) ai_baset inline

operator[](locationt l) const ait< domainT > inline

output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const ai_baset virtual

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

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

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

output_json(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const ai_baset virtual

output_json(const namespacet &ns, const goto_functionst &goto_functions) const ai_baset virtual

output_json(const goto_modelt &goto_model) const ai_baset inline

output_json(const namespacet &ns, const goto_programt &goto_program) const ai_baset inline

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

output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const ai_baset virtual

output_xml(const namespacet &ns, const goto_functionst &goto_functions) const ai_baset virtual

output_xml(const goto_modelt &goto_model) const ai_baset inline

output_xml(const namespacet &ns, const goto_programt &goto_program) const ai_baset inline

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

put_in_working_set(working_sett &working_set, trace_ptrt t) ai_baset inlineprotected

statet typedef ai_baset

storage ai_baset protected

trace_ptrt typedef ai_baset

trace_sett typedef ai_baset

visit(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) ai_baset protectedvirtual

visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set) ai_baset protected

visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override ai_recursive_interproceduralt protectedvirtual

visit_end_function(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) ai_baset protectedvirtual

visit_function_call(const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) ai_baset protectedvirtual

working_sett typedef ai_baset protected

~ai_baset() ai_baset inlinevirtual