cprover
|
#include "show_vcc.h"
#include "symex_target_equation.h"
#include <fstream>
#include <iostream>
#include <sstream>
#include <util/exception_utils.h>
#include <util/format_expr.h>
#include <util/json.h>
#include <util/json_expr.h>
#include <util/ui_message.h>
Go to the source code of this file.
Functions | |
void | show_vcc_plain (messaget::mstreamt &out, const symex_target_equationt &equation) |
void | show_vcc_json (std::ostream &out, const symex_target_equationt &equation) |
void | show_vcc (const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation) |
Output of the verification conditions (VCCs)
Definition in file show_vcc.cpp.
void show_vcc | ( | const optionst & | options, |
ui_message_handlert & | ui_message_handler, | ||
const symex_target_equationt & | equation | ||
) |
Definition at line 161 of file show_vcc.cpp.
void show_vcc_json | ( | std::ostream & | out, |
const symex_target_equationt & | equation | ||
) |
Definition at line 103 of file show_vcc.cpp.
void show_vcc_plain | ( | messaget::mstreamt & | out, |
const symex_target_equationt & | equation | ||
) |
Definition at line 27 of file show_vcc.cpp.