how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override

jsont output_json (const ai_baset &ai, const namespacet &ns) const override

Outputs the current value of the domain.

void make_top () final override

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

void make_bottom () final override

no states

void make_entry () final override

Make this domain a reasonable entry-point state For most domains top is sufficient.

bool is_top () const final override

bool is_bottom () const final override

node_indext get_node_id () const

void populate_dep_graph (dependence_grapht &, goto_programt::const_targett) const

- Public Member Functions inherited from ai_domain_baset

virtual ~ai_domain_baset ()

virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const

virtual bool ai_simplify (exprt &condition, const namespacet &) const

also add

virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const

Simplifies the expression but keeps it as an l-value.

virtual exprt to_predicate (void) const

Gives a Boolean condition that is true for all values represented by the domain.

Private Types

typedef std::set< goto_programt::const_targett, goto_programt::target_less_than > depst

Private Member Functions

void control_dependencies (const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)

void data_dependencies (goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)

Private Attributes

tvt has_values

node_indext node_id

bool has_changed

depst control_deps

depst control_dep_candidates

depst data_deps

message_handlert & message_handler

Friends

const depst & dependence_graph_test_get_control_deps (const dep_graph_domaint &)

const depst & dependence_graph_test_get_data_deps (const dep_graph_domaint &)

Additional Inherited Members

- Protected Member Functions inherited from ai_domain_baset

ai_domain_baset ()

The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface.

ai_domain_baset (const ai_domain_baset &old)

A copy constructor is part of the domain interface.

Detailed Description

Definition at line 66 of file dependence_graph.h.

Member Typedef Documentation

◆ depst

typedef std:: set<goto_programt::const_targett, goto_programt::target_less_than> dep_graph_domaint::depst

private

Definition at line 180 of file dependence_graph.h.

◆ node_indext

typedef grapht<dep_nodet>::node_indext dep_graph_domaint::node_indext

Definition at line 69 of file dependence_graph.h.

Constructor & Destructor Documentation

◆ dep_graph_domaint()

dep_graph_domaint::dep_graph_domaint ( node_indext id,

message_handlert & message_handler

)

inline

Definition at line 71 of file dependence_graph.h.

Member Function Documentation

◆ control_dependencies()

void dep_graph_domaint::control_dependencies ( const irep_idt & function_id,

goto_programt::const_targett from,

goto_programt::const_targett to,

dependence_grapht & dep_graph

)

private

Definition at line 52 of file dependence_graph.cpp.

◆ data_dependencies()

void dep_graph_domaint::data_dependencies ( goto_programt::const_targett from,

const irep_idt & function_to,

goto_programt::const_targett to,

dependence_grapht & dep_graph,

const namespacet & ns

)

private

Definition at line 154 of file dependence_graph.cpp.

◆ get_node_id()

node_indext dep_graph_domaint::get_node_id ( ) const

inline

Definition at line 164 of file dependence_graph.h.

◆ is_bottom()

bool dep_graph_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 150 of file dependence_graph.h.

◆ is_top()

bool dep_graph_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 136 of file dependence_graph.h.

◆ make_bottom()

void dep_graph_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 109 of file dependence_graph.h.

◆ make_entry()

void dep_graph_domaint::make_entry ( )

inlinefinaloverridevirtual

Make this domain a reasonable entry-point state For most domains top is sufficient.

Reimplemented from ai_domain_baset.

Definition at line 122 of file dependence_graph.h.

◆ make_top()

void dep_graph_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 98 of file dependence_graph.h.

◆ merge()

bool dep_graph_domaint::merge ( const dep_graph_domaint & src,

trace_ptrt from,

trace_ptrt to

)

Definition at line 22 of file dependence_graph.cpp.

◆ output()

void dep_graph_domaint::output ( std::ostream & out,

const ai_baset & ai,

const namespacet & ns

) const

finaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 272 of file dependence_graph.cpp.

◆ output_json()

jsont dep_graph_domaint::output_json ( const ai_baset & ai,

const namespacet & ns

) const

overridevirtual

Outputs the current value of the domain.

parameters: The abstract interpreter and the namespace.

Returns: The domain, formatted as a JSON object.

Reimplemented from ai_domain_baset.

Definition at line 311 of file dependence_graph.cpp.

◆ populate_dep_graph()

void dep_graph_domaint::populate_dep_graph ( dependence_grapht & dep_graph,

goto_programt::const_targett this_loc

) const

Definition at line 393 of file dependence_graph.cpp.

◆ transform()

void dep_graph_domaint::transform ( const irep_idt & function_from,

trace_ptrt from,

const irep_idt & function_to,

trace_ptrt to,

ai_baset & ai,

const namespacet & ns

)

finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implements ai_domain_baset.

Definition at line 217 of file dependence_graph.cpp.

Friends And Related Symbol Documentation

◆ dependence_graph_test_get_control_deps

const depst & dependence_graph_test_get_control_deps ( const dep_graph_domaint & )

friend

◆ dependence_graph_test_get_data_deps

const depst & dependence_graph_test_get_data_deps ( const dep_graph_domaint & )

friend

Member Data Documentation

◆ control_dep_candidates

depst dep_graph_domaint::control_dep_candidates

private

Definition at line 189 of file dependence_graph.h.

◆ control_deps

depst dep_graph_domaint::control_deps

private

Definition at line 184 of file dependence_graph.h.

◆ data_deps

depst dep_graph_domaint::data_deps

private

Definition at line 193 of file dependence_graph.h.

◆ has_changed

bool dep_graph_domaint::has_changed

private

Definition at line 176 of file dependence_graph.h.

◆ has_values

tvt dep_graph_domaint::has_values

private

Definition at line 174 of file dependence_graph.h.

◆ message_handler

message_handlert& dep_graph_domaint::message_handler

private

Definition at line 195 of file dependence_graph.h.

◆ node_id

node_indext dep_graph_domaint::node_id

private

Definition at line 175 of file dependence_graph.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/dependence_graph.h
/home/runner/work/cbmc/cbmc/src/analyses/dependence_graph.cpp