cprover
show_vcc.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Output of the verification conditions (VCCs)
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_SYMEX_SHOW_VCC_H
13
#define CPROVER_GOTO_SYMEX_SHOW_VCC_H
14
15
#include <
util/ui_message.h
>
16
17
class
optionst
;
18
class
symex_target_equationt
;
19
26
void
show_vcc
(
27
const
optionst
&options,
28
ui_message_handlert
&ui_message_handler,
29
const
symex_target_equationt
&equation);
30
31
#endif // CPROVER_GOTO_SYMEX_SHOW_VCC_H
ui_message_handlert
Definition:
ui_message.h:20
optionst
Definition:
options.h:23
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:41
show_vcc
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Definition:
show_vcc.cpp:169
ui_message.h
goto-symex
show_vcc.h
Generated by
1.8.20