Loading...

Searching...

No Matches

Public Member Functions | Protected Attributes | List of all members

encoding_targett Class Referenceabstract

#include <state_encoding_targets.h>

+ Inheritance diagram for encoding_targett:

[フレーム]

[legend]

+ Collaboration diagram for encoding_targett:

[フレーム]

[legend]

Public Member Functions

virtual void annotation (const std::string &)

virtual void set_to_true (source_locationt, exprt)=0

void set_to_true (exprt expr)

void set_source_location (source_locationt __source_location)

virtual ~encoding_targett ()=default

virtual void annotation (const std::string &)

virtual void set_to_true (source_locationt, exprt)=0

void set_to_true (exprt expr)

void set_source_location (source_locationt __source_location)

virtual ~encoding_targett ()=default

Protected Attributes

source_locationt source_location = source_locationt::nil()

Detailed Description

Definition at line 16 of file state_encoding_targets.h.

Constructor & Destructor Documentation

◆ ~encoding_targett() [1/2]

virtual encoding_targett::~encoding_targett ( )

virtualdefault

◆ ~encoding_targett() [2/2]

virtual encoding_targett::~encoding_targett ( )

virtualdefault

Member Function Documentation

◆ annotation() [1/2]

virtual void encoding_targett::annotation ( const std::string & )

inlinevirtual

Reimplemented in smt2_encoding_targett, ascii_encoding_targett, smt2_encoding_targett, and ascii_encoding_targett.

Definition at line 19 of file state_encoding_targets.h.

◆ annotation() [2/2]

virtual void encoding_targett::annotation ( const std::string & )

inlinevirtual

Reimplemented in smt2_encoding_targett, ascii_encoding_targett, smt2_encoding_targett, and ascii_encoding_targett.

Definition at line 217 of file horn_encoding.cpp.

◆ set_source_location() [1/2]

void encoding_targett::set_source_location ( source_locationt __source_location )

inline

Definition at line 30 of file state_encoding_targets.h.

◆ set_source_location() [2/2]

void encoding_targett::set_source_location ( source_locationt __source_location )

inline

Definition at line 228 of file horn_encoding.cpp.

◆ set_to_true() [1/4]

void encoding_targett::set_to_true ( exprt expr )

inline

Definition at line 25 of file state_encoding_targets.h.

◆ set_to_true() [2/4]

void encoding_targett::set_to_true ( exprt expr )

inline

Definition at line 223 of file horn_encoding.cpp.

◆ set_to_true() [3/4]

virtual void encoding_targett::set_to_true ( source_locationt ,

exprt

)

pure virtual

Implemented in container_encoding_targett, container_encoding_targett, smt2_encoding_targett, smt2_encoding_targett, ascii_encoding_targett, and ascii_encoding_targett.

◆ set_to_true() [4/4]

virtual void encoding_targett::set_to_true ( source_locationt ,

exprt

)

pure virtual

Implemented in container_encoding_targett, container_encoding_targett, smt2_encoding_targett, smt2_encoding_targett, ascii_encoding_targett, and ascii_encoding_targett.

Member Data Documentation

◆ source_location

source_locationt encoding_targett::source_location = source_locationt::nil()

protected

Definition at line 38 of file state_encoding_targets.h.

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

/home/runner/work/cbmc/cbmc/src/cprover/state_encoding_targets.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/horn_encoding.cpp