cprover
show_program.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Output of the program (SSA) constraints
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_SYMEX_SHOW_PROGRAM_H
13
#define CPROVER_GOTO_SYMEX_SHOW_PROGRAM_H
14
15
class
namespacet
;
16
class
symex_target_equationt
;
17
18
void
show_program
(
const
namespacet
&ns,
const
symex_target_equationt
&equation);
19
20
#endif // CPROVER_GOTO_SYMEX_SHOW_PROGRAM_H
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Definition:
show_program.cpp:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition:
symex_target_equation.h:35
goto-symex
show_program.h
Generated by
1.8.17