Loading...

Searching...

No Matches

graphml_witness.cpp File Reference

Witnesses for Traces and Proofs. More...

#include "graphml_witness.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/find_symbols.h>
#include <util/namespace.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
#include <util/symbol.h>
#include <ansi-c/expr2c.h>
#include <goto-symex/symex_target_equation.h>
#include <langapi/language_util.h>
#include <langapi/mode.h>
#include "goto_program.h"
#include "goto_trace.h"

+ Include dependency graph for graphml_witness.cpp:

[フレーム]

Go to the source code of this file.

Functions

static std::string expr_to_string (const namespacet &ns, const irep_idt &id, const exprt &expr)

static bool filter_out (const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)

static bool contains_symbol_prefix (const exprt &expr, const std::string &prefix)

static bool is_function_built_in_or_extern (const namespacet &ns, const irep_idt &function_id)

Check if a function is built-in (CPROVER library), has no body, or does not exist in the symbol table.

static bool all_symbols_in_scope (const exprt &expr, const irep_idt &function_id)

Check if all symbols in an expression are in scope.

Detailed Description

Witnesses for Traces and Proofs.

Definition in file graphml_witness.cpp.

Function Documentation

◆ all_symbols_in_scope()

static bool all_symbols_in_scope ( const exprt & expr,

const irep_idt & function_id

)

static

Check if all symbols in an expression are in scope.

Note: scope is determined by the prefix before the first "::". This is correct for CBMC's C front-end where locals are named "function::N::var" and function_id is "function". JBMC does not use graphml witnesses.

Definition at line 303 of file graphml_witness.cpp.

◆ contains_symbol_prefix()

static bool contains_symbol_prefix ( const exprt & expr,

const std::string & prefix

)

static

Definition at line 260 of file graphml_witness.cpp.

◆ expr_to_string()

static std::string expr_to_string ( const namespacet & ns,

const irep_idt & id,

const exprt & expr

)

static

Definition at line 35 of file graphml_witness.cpp.

◆ filter_out()

static bool filter_out ( const goto_tracet & goto_trace,

const goto_tracet::stepst::const_iterator & prev_it,

goto_tracet::stepst::const_iterator & it

)

static

Definition at line 217 of file graphml_witness.cpp.

◆ is_function_built_in_or_extern()

static bool is_function_built_in_or_extern ( const namespacet & ns,

const irep_idt & function_id

)

static

Check if a function is built-in (CPROVER library), has no body, or does not exist in the symbol table.

Definition at line 279 of file graphml_witness.cpp.