CBMC
show_vcc.h File Reference

Output of the verification conditions (VCCs) More...

+ This graph shows which files directly or indirectly include this file:

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...
 

Detailed Description

Output of the verification conditions (VCCs)

Definition in file show_vcc.h.

Function Documentation

◆ 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.

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.