static_verifier.cpp File Reference

#include "static_verifier.h"
#include <util/json_irep.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/options.h>
#include <util/range.h>
#include <util/xml_irep.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.

Functions
std::string	as_string (const ai_verifier_statust &status)
	Makes a status message string from a status.
static ai_verifier_statust	check_assertion (const ai_domain_baset &domain, exprt e, const namespacet &ns)
void	static_verifier (const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
	Use the information from the abstract interpreter to fill out the statuses of the passed properties.
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.

Function Documentation

as_string()

std::string as_string

(

const ai_verifier_statust &

status

)

Makes a status message string from a status.

Definition at line 23 of file static_verifier.cpp.

check_assertion()

ai_verifier_statust check_assertion ( const ai_domain_baset & domain, exprt e, const namespacet & ns )

static

Definition at line 87 of file static_verifier.cpp.

static_verifier() [1/2]

void static_verifier	(	const abstract_goto_modelt &	abstract_goto_model,
		const ai_baset &	ai,
		propertiest &	properties )

Use the information from the abstract interpreter to fill out the statuses of the passed properties.

Parameters

abstract_goto_model	The goto program to verify
ai	The abstract interpreter (should be run to fixpoint before calling this function)
properties	The properties to fill out

Definition at line 229 of file static_verifier.cpp.

static_verifier() [2/2]

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_model	the program analyzed
ai	the abstract interpreter after it has been run to fix point
options	the parsed user options
message_handler	the system message handler
out	output stream for the printing

Returns

false on success with the domain printed to out

Definition at line 403 of file static_verifier.cpp.

static_verifier_console()

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

static

Definition at line 326 of file static_verifier.cpp.

static_verifier_json()

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

static

Definition at line 270 of file static_verifier.cpp.

static_verifier_text()

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

static

Definition at line 297 of file static_verifier.cpp.

static_verifier_xml()

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

static

Definition at line 283 of file static_verifier.cpp.