cegis_verifier.cpp File Reference

Verifier for Counterexample-Guided Synthesis. More...

#include "cegis_verifier.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/options.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <goto-programs/pointer_arithmetic.h>
#include <goto-programs/process_goto_program.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/set_properties.h>
#include <analyses/dependence_graph.h>
#include <ansi-c/cprover_library.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <ansi-c/goto-conversion/link_to_library.h>
#include <assembler/remove_asm.h>
#include <cpp/cprover_library.h>
#include <goto-checker/all_properties_verifier_with_trace_storage.h>
#include <goto-checker/multi_path_symex_checker.h>
#include <goto-instrument/contracts/contracts.h>
#include <goto-instrument/contracts/instrument_spec_assigns.h>
#include <goto-instrument/contracts/utils.h>
#include <goto-instrument/havoc_utils.h>
#include <langapi/language_util.h>
#include <pointer-analysis/add_failed_symbols.h>
#include <solvers/prop/prop.h>

Include dependency graph for cegis_verifier.cpp:

Go to the source code of this file.

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

Detailed Description

Verifier for Counterexample-Guided Synthesis.

Definition in file cegis_verifier.cpp.

Function Documentation

contains_symbol_prefix()

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

static

Definition at line 41 of file cegis_verifier.cpp.

get_checked_pointer_from_null_pointer_check()

static const exprt& get_checked_pointer_from_null_pointer_check ( const exprt &  violation )

static

Definition at line 56 of file cegis_verifier.cpp.