CBMC
|
Output of the verification conditions (VCCs) More...
Go to the source code of this file.
Functions | |
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. More... | |
Output of the verification conditions (VCCs)
Definition in file show_vcc.h.
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.
The name of the output file is given by the outfile
option from options
, the standard input is used if it is not provided. The format is either JSON or plain text depending on ui_message_handler
; XML is not supported. See show_vcc_json and show_vcc_plain
Definition at line 168 of file show_vcc.cpp.