CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/path.h Source File

22 class path_nodet

23{

24public:

30

37

38 void output(const goto_programt &program, std::ostream &str) const;

39

40 goto_programt::targett loc;

41 const exprt guard;

42};

ait

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

Definition ai.h:566

exprt

Base class for all expressions.

Definition expr.h:57

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

goto_programt::targett

instructionst::iterator targett

Definition goto_program.h:613

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

nil_exprt

The NIL expression.

Definition std_expr.h:3144

path_nodet

Definition path.h:23

path_nodet::loc

goto_programt::targett loc

Definition path.h:40

path_nodet::path_nodet

path_nodet(const goto_programt::targett &_loc, const exprt &_guard)

Definition path.h:31

path_nodet::guard

const exprt guard

Definition path.h:41

path_nodet::path_nodet

path_nodet(const goto_programt::targett &_loc)

Definition path.h:25

path_nodet::output

void output(const goto_programt &program, std::ostream &str) const

goto_program.h

Concrete Goto Program.

output_path

void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)

pathst

std::list< patht > pathst

Definition path.h:45

patht

std::list< path_nodet > patht

Definition path.h:44

std_expr.h

API to expression classes.