CBMC
symex_target.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "symex_target.h"
13 
14 bool 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 }
goto_programt::target_less_than
instructiont::target_less_than target_less_than
Definition: goto_program.h:619
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:38
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:42
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.