Class recording the outcome of symbolic execution. More...

#include <goto_symex.h>

Public Member Functions
	symex_resultt (std::shared_ptr< symex_targett > t, unsigned int claims, unsigned int remain, unsigned int simplified, unsigned int truncations=0)

Public Attributes
std::shared_ptr< symex_targett >	target
unsigned int	total_claims
unsigned int	remaining_claims
unsigned int	simplified_claims
unsigned int	bounded_loop_truncations
	Carried out of exploration rather than read back from live state: under –schedule the current frame is already dangling by the time bmct looks (issue #6423).

Detailed Description

Class recording the outcome of symbolic execution.

Contains the things that are of interest to the BMC class: The object containing the symex equation (or otherwise, the symex target), as well as the list of claims that have been recorded (and how many are already satisfied).

Constructor & Destructor Documentation

◆ symex_resultt()

goto_symext::symex_resultt::symex_resultt	(	std::shared_ptr< symex_targett >	t,
		unsigned int	claims,
		unsigned int	remain,
		unsigned int	simplified,
		unsigned int	truncations = 0 )

inline

Member Data Documentation

◆ bounded_loop_truncations

unsigned int goto_symext::symex_resultt::bounded_loop_truncations

Carried out of exploration rather than read back from live state: under –schedule the current frame is already dangling by the time bmct looks (issue #6423).

◆ remaining_claims

unsigned int goto_symext::symex_resultt::remaining_claims

◆ simplified_claims

unsigned int goto_symext::symex_resultt::simplified_claims

◆ target

std::shared_ptr<symex_targett> goto_symext::symex_resultt::target

◆ total_claims

unsigned int goto_symext::symex_resultt::total_claims

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

src/goto-symex/engine/goto_symex.h

Public Member Functions

Public Attributes