CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_target.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "symex_target.h"
13
14bool operator<(
15 const symex_targett::sourcet &a,
16 const symex_targett::sourcet &b)
17{
18 if(a.thread_nr==b.thread_nr)
19 return goto_programt::target_less_than()(a.pc, b.pc);
20 else
21 return a.thread_nr < b.thread_nr;
22}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_programt::target_less_than
instructiont::target_less_than target_less_than
Definition goto_program.h:618
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition symex_target.h:37
operator<
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
Base class comparison operator for symbolic execution targets.
Definition symex_target.cpp:14
symex_target.h
Generate Equation using Symbolic Execution.