CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt_logics.cpp File Reference
#include "smt_logics.h"
#include "smt_logics.def"
+ Include dependency graph for smt_logics.cpp:

Go to the source code of this file.

Macros

#define LOGIC_ID(the_id, the_name)    const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
 
#define LOGIC_ID(the_id, the_name)
 
#define LOGIC_ID(the_id, the_name)
 

Functions

template<typename visitort >
void accept (const smt_logict &logic, const irep_idt &id, visitort &&visitor)
 

Macro Definition Documentation

◆ LOGIC_ID [1/3]

#define LOGIC_ID (   the_id,
  the_name 
)     const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};

Definition at line 6 of file smt_logics.cpp.

◆ LOGIC_ID [2/3]

#define LOGIC_ID (   the_id,
  the_name 
)
Value:
if(id == ID_smt_logic_##the_id) \
return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
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:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

Definition at line 6 of file smt_logics.cpp.

◆ LOGIC_ID [3/3]

#define LOGIC_ID (   the_id,
  the_name 
)
Value:
smt_logic_##the_id##t::smt_logic_##the_id##t() \
{ \
}

Definition at line 6 of file smt_logics.cpp.

Function Documentation

◆ accept()

template<typename visitort >
void accept ( const smt_logict logic,
const irep_idt id,
visitort &&  visitor 
)

Definition at line 23 of file smt_logics.cpp.