Counterexample Found. More...

#include "counterexample_found.h"
#include <util/cout_message.h>
#include <util/simplify_expr.h>
#include <solvers/sat/satcheck.h>
#include "axioms.h"
#include "bv_pointers_wide.h"
#include "simplify_state_expr.h"
#include "state.h"

Include dependency graph for counterexample_found.cpp:

Go to the source code of this file.

Functions
void	show_assignment (const bv_pointers_widet &solver)

static exprt	evaluator_rec (const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)

static exprt	evaluator (const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)

propertyt::tracet	counterexample (const std::vector< framet > &frames, const workt &work, const bv_pointers_widet &solver, const axiomst &axioms, const namespacet &ns)

std::optional< propertyt::tracet >	counterexample_found (const std::vector< framet > &frames, const workt &work, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)

Detailed Description

Counterexample Found.

Definition in file counterexample_found.cpp.

Function Documentation

◆ counterexample()

propertyt::tracet counterexample	(	const std::vector< framet > &	frames,
		const workt &	work,
		const bv_pointers_widet &	solver,
		const axiomst &	axioms,
		const namespacet &	ns
	)

Definition at line 106 of file counterexample_found.cpp.

◆ counterexample_found()

std::optional< propertyt::tracet > counterexample_found	(	const std::vector< framet > &	frames,
		const workt &	work,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		bool	verbose,
		const namespacet &	ns
	)

Definition at line 173 of file counterexample_found.cpp.

◆ evaluator()

static exprt evaluator	(	const std::unordered_map< exprt, exprt, irep_hash > &	memory,
		const decision_proceduret &	solver,
		exprt	src,
		const namespacet &	ns
	)

static

Definition at line 96 of file counterexample_found.cpp.

◆ evaluator_rec()

static exprt evaluator_rec	(	const std::unordered_map< exprt, exprt, irep_hash > &	memory,
		const decision_proceduret &	solver,
		exprt	src,
		const namespacet &	ns
	)

static

Definition at line 59 of file counterexample_found.cpp.

◆ show_assignment()

void show_assignment ( const bv_pointers_widet & solver )

Definition at line 24 of file counterexample_found.cpp.