Loading...

Searching...

No Matches

uninitialized_domaint Class Reference

#include <uninitialized_domain.h>

+ Inheritance diagram for uninitialized_domaint:

[フレーム]

[legend]

+ Collaboration diagram for uninitialized_domaint:

[フレーム]

[legend]

Public Types

typedef std::set< irep_idt > uninitializedt

- Public Types inherited from ai_domain_baset

typedef goto_programt::const_targett locationt

typedef ai_history_baset::trace_ptrt trace_ptrt

Public Member Functions

uninitialized_domaint ()

void transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override

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

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

bool is_top () const override final

bool is_bottom () const override final

bool merge (const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to)

- Public Member Functions inherited from ai_domain_baset

virtual ~ai_domain_baset ()

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

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

virtual void make_entry ()

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

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.

Public Attributes

uninitializedt uninitialized

Private Member Functions

void assign (const exprt &lhs)

Private Attributes

tvt has_values

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 21 of file uninitialized_domain.h.

Member Typedef Documentation

◆ uninitializedt

typedef std::set<irep_idt> uninitialized_domaint::uninitializedt

Definition at line 29 of file uninitialized_domain.h.

Constructor & Destructor Documentation

◆ uninitialized_domaint()

uninitialized_domaint::uninitialized_domaint ( )

inline

Definition at line 24 of file uninitialized_domain.h.

Member Function Documentation

◆ assign()

void uninitialized_domaint::assign ( const exprt & lhs )

private

Definition at line 55 of file uninitialized_domain.cpp.

◆ is_bottom()

bool uninitialized_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 64 of file uninitialized_domain.h.

◆ is_top()

bool uninitialized_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 57 of file uninitialized_domain.h.

◆ make_bottom()

void uninitialized_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 51 of file uninitialized_domain.h.

◆ make_top()

void uninitialized_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 45 of file uninitialized_domain.h.

◆ merge()

bool uninitialized_domaint::merge ( const uninitialized_domaint & other,

trace_ptrt from,

trace_ptrt to

)

Returns: returns true iff there is something new

Definition at line 80 of file uninitialized_domain.cpp.

◆ output()

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

const ai_baset & ai,

const namespacet & ns

) const

finalvirtual

Reimplemented from ai_domain_baset.

Definition at line 65 of file uninitialized_domain.cpp.

◆ transform()

void uninitialized_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 20 of file uninitialized_domain.cpp.

Member Data Documentation

◆ has_values

tvt uninitialized_domaint::has_values

private

Definition at line 76 of file uninitialized_domain.h.

◆ uninitialized

uninitializedt uninitialized_domaint::uninitialized

Definition at line 30 of file uninitialized_domain.h.

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

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