CBMC
symex_target.h File Reference

Generate Equation using Symbolic Execution. More...

+ Include dependency graph for symex_target.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  symex_targett
 The interface of the target container for symbolic execution to record its symbolic steps into. More...
 
struct  symex_targett::sourcet
 Identifies source in the context of symbolic execution. More...
 

Functions

bool operator< (const symex_targett::sourcet &a, const symex_targett::sourcet &b)
 Base class comparison operator for symbolic execution targets. More...
 

Detailed Description

Generate Equation using Symbolic Execution.

Definition in file symex_target.h.

Function Documentation

◆ operator<()

bool operator< ( const symex_targett::sourcet a,
const symex_targett::sourcet b 
)

Base class comparison operator for symbolic execution targets.

Order first by thread numbers and then by program counters.

Parameters
aLeft-hand target
bRight-hand target
Returns
True if a precedes b.

Definition at line 14 of file symex_target.cpp.