cprover
static_verifier.cpp File Reference
#include "static_verifier.h"
#include <util/json_expr.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/options.h>
#include <goto-programs/goto_model.h>
#include <analyses/ai.h>
+ Include dependency graph for static_verifier.cpp:

Go to the source code of this file.

Classes

struct  static_verifier_resultt
 

Functions

static void static_verifier_json (const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
 
static void static_verifier_xml (const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
 
static void static_verifier_text (const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
 
static void static_verifier_console (const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
 
bool static_verifier (const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
 Runs the analyzer and then prints out the domain. More...
 

Function Documentation

◆ static_verifier()

bool static_verifier ( const goto_modelt goto_model,
const ai_baset ai,
const optionst options,
message_handlert message_handler,
std::ostream &  out 
)

Runs the analyzer and then prints out the domain.

Parameters
goto_modelthe program analyzed
aithe abstract interpreter after it has been run to fix point
optionsthe parsed user options
message_handlerthe system message handler
outoutput stream for the printing
Returns
: false on success with the domain printed to out

Definition at line 234 of file static_verifier.cpp.

◆ static_verifier_console()

static void static_verifier_console ( const std::vector< static_verifier_resultt > &  results,
const namespacet ns,
messaget m 
)
static

Definition at line 157 of file static_verifier.cpp.

◆ static_verifier_json()

static void static_verifier_json ( const std::vector< static_verifier_resultt > &  results,
messaget m,
std::ostream &  out 
)
static

Definition at line 29 of file static_verifier.cpp.

◆ static_verifier_text()

static void static_verifier_text ( const std::vector< static_verifier_resultt > &  results,
const namespacet ns,
std::ostream &  out 
)
static

Definition at line 107 of file static_verifier.cpp.

◆ static_verifier_xml()

static void static_verifier_xml ( const std::vector< static_verifier_resultt > &  results,
messaget m,
std::ostream &  out 
)
static

Definition at line 67 of file static_verifier.cpp.