Formatted counterexample. More...

#include <cegis_verifier.h>

Collaboration diagram for cext:

Public Types
enum class	violation_typet { cex_out_of_boundary , cex_null_pointer , cex_not_preserved , cex_not_hold_upon_entry , cex_assignable , cex_other }

enum class	violation_locationt { in_loop , after_loop , in_condition }

Public Member Functions
	cext (const std::unordered_map< exprt, mp_integer, irep_hash > &object_sizes, const std::unordered_map< exprt, mp_integer, irep_hash > &havoced_values, const std::unordered_map< exprt, mp_integer, irep_hash > &havoced_pointer_offsets, const std::unordered_map< exprt, mp_integer, irep_hash > &loop_entry_values, const std::unordered_map< exprt, mp_integer, irep_hash > &loop_entry_offsets, const std::set< exprt > &live_variables)

	cext (const violation_typet &violation_type)

Public Attributes
exprt	checked_pointer

exprt	violated_predicate

violation_locationt	violation_location = violation_locationt::in_loop

std::unordered_map< exprt, mp_integer, irep_hash >	object_sizes

std::unordered_map< exprt, mp_integer, irep_hash >	havoced_values

std::unordered_map< exprt, mp_integer, irep_hash >	havoced_pointer_offsets

std::unordered_map< exprt, mp_integer, irep_hash >	loop_entry_values

std::unordered_map< exprt, mp_integer, irep_hash >	loop_entry_offsets

std::set< exprt >	live_variables

violation_typet	violation_type

std::list< loop_idt >	cause_loop_ids

Detailed Description

Formatted counterexample.

Definition at line 25 of file cegis_verifier.h.

Member Enumeration Documentation

◆ violation_locationt

enum class cext::violation_locationt

strong

Enumerator
in_loop
after_loop
in_condition

Definition at line 38 of file cegis_verifier.h.

◆ violation_typet

enum class cext::violation_typet

strong

Enumerator
cex_out_of_boundary
cex_null_pointer
cex_not_preserved
cex_not_hold_upon_entry
cex_assignable
cex_other

Definition at line 28 of file cegis_verifier.h.

Constructor & Destructor Documentation

◆ cext() [1/2]

cext::cext	(	const std::unordered_map< exprt, mp_integer, irep_hash > &	object_sizes,
		const std::unordered_map< exprt, mp_integer, irep_hash > &	havoced_values,
		const std::unordered_map< exprt, mp_integer, irep_hash > &	havoced_pointer_offsets,
		const std::unordered_map< exprt, mp_integer, irep_hash > &	loop_entry_values,
		const std::unordered_map< exprt, mp_integer, irep_hash > &	loop_entry_offsets,
		const std::set< exprt > &	live_variables
	)

inline

Definition at line 45 of file cegis_verifier.h.

◆ cext() [2/2]

cext::cext ( const violation_typet & violation_type )

inlineexplicit

Definition at line 62 of file cegis_verifier.h.

Member Data Documentation

◆ cause_loop_ids

std::list<loop_idt> cext::cause_loop_ids

Definition at line 94 of file cegis_verifier.h.

◆ checked_pointer

exprt cext::checked_pointer

Definition at line 68 of file cegis_verifier.h.

◆ havoced_pointer_offsets

std::unordered_map<exprt, mp_integer, irep_hash> cext::havoced_pointer_offsets

Definition at line 82 of file cegis_verifier.h.

◆ havoced_values

std::unordered_map<exprt, mp_integer, irep_hash> cext::havoced_values

Definition at line 80 of file cegis_verifier.h.

◆ live_variables

std::set<exprt> cext::live_variables

Definition at line 91 of file cegis_verifier.h.

◆ loop_entry_offsets

std::unordered_map<exprt, mp_integer, irep_hash> cext::loop_entry_offsets

Definition at line 88 of file cegis_verifier.h.

◆ loop_entry_values

std::unordered_map<exprt, mp_integer, irep_hash> cext::loop_entry_values

Definition at line 86 of file cegis_verifier.h.

◆ object_sizes

std::unordered_map<exprt, mp_integer, irep_hash> cext::object_sizes

Definition at line 78 of file cegis_verifier.h.

◆ violated_predicate

exprt cext::violated_predicate

Definition at line 69 of file cegis_verifier.h.

◆ violation_location

violation_locationt cext::violation_location = violation_locationt::in_loop

Definition at line 72 of file cegis_verifier.h.

◆ violation_type

violation_typet cext::violation_type

Definition at line 93 of file cegis_verifier.h.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/src/goto-synthesizer/cegis_verifier.h

Public Types

Public Member Functions

Public Attributes