CBMC
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 class optionst;
16 class symex_target_equationt;
17 class ui_message_handlert;
18 
25 void show_vcc(
26  const optionst &options,
27  ui_message_handlert &ui_message_handler,
28  const symex_target_equationt &equation);
29 
30 #endif // CPROVER_GOTO_SYMEX_SHOW_VCC_H
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:34
ui_message_handlert
Definition: ui_message.h:22
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:168