Loading...

Searching...

No Matches

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()

static 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()

static 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()

static 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()

static 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()

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