CBMC: /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/ast/smt_sorts.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Macros | Functions

smt_sorts.cpp File Reference

#include "smt_sorts.h"
#include <util/invariant.h>
#include "smt_sorts.def"

+ Include dependency graph for smt_sorts.cpp:

Go to the source code of this file.

Macros

#define SORT_ID(the_id) const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};

#define SORT_ID(the_id)

#define SORT_ID(the_id)

#define SORT_ID(the_id)

Functions

template<typename visitort >

void accept (const smt_sortt &sort, const irep_idt &id, visitort &&visitor)

Macro Definition Documentation

◆ SORT_ID [1/4]

#define SORT_ID ( the_id ) const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};

Definition at line 8 of file smt_sorts.cpp.

◆ SORT_ID [2/4]

#define SORT_ID ( the_id )

Value:

template <> \

const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const & \

{ \

return id() == ID_smt_##the_id##_sort \

? static_cast<const smt_##the_id##_sortt *>(this) \

}

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

const irep_idt & id() const

Definition irep.h:388

Definition at line 8 of file smt_sorts.cpp.

◆ SORT_ID [3/4]

#define SORT_ID ( the_id )

Value:

template <> \

std::optional<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() \

&& \

{ \

if(id() == ID_smt_##the_id##_sort) \

return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))}; \

}

Definition at line 8 of file smt_sorts.cpp.

◆ SORT_ID [4/4]

#define SORT_ID ( the_id )

Value:

if(id == ID_smt_##the_id##_sort) \

return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));

ai_baset::visit

virtual bool 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)

Perform one step of abstract interpretation from trace t Depending on the instruction type it may com...

Definition ai.cpp:270

Definition at line 8 of file smt_sorts.cpp.

Function Documentation

◆ accept()

template<typename visitort >

void accept ( const smt_sortt & sort,

const irep_idt & id,

visitort && visitor

)

Definition at line 87 of file smt_sorts.cpp.