claim_slicer Class Reference

Claim slicer: remove every other claim of the formula with the exception of the one to keep. More...

#include <slice.h>

Inheritance diagram for claim_slicer:

Public Member Functions
	claim_slicer (const size_t claim_to_keep, bool show_slice_info, bool is_goto_cov, namespacet &ns)
bool	run (symex_target_equationt::SSA_stepst &) override
	Executes the algorithm over a T object.
Public Member Functions inherited from slicer
	slicer ()
BigInt	ignored () const override
	How many steps were ignored after this algorithm.
Public Member Functions inherited from ssa_step_algorithm
	ssa_step_algorithm (bool sideffect)
void	run_on_step (symex_target_equationt::SSA_stept &)
virtual void	run_on_assignment (symex_target_equationt::SSA_stept &)
virtual void	run_on_assume (symex_target_equationt::SSA_stept &)
virtual void	run_on_assert (symex_target_equationt::SSA_stept &)
virtual void	run_on_output (symex_target_equationt::SSA_stept &)
virtual void	run_on_skip (symex_target_equationt::SSA_stept &)
virtual void	run_on_renumber (symex_target_equationt::SSA_stept &)
virtual void	run_on_branching (symex_target_equationt::SSA_stept &)
Public Member Functions inherited from algorithm< symex_target_equationt::SSA_stepst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Public Attributes
size_t	claim_to_keep
std::string	claim_msg
std::string	claim_loc
std::string	claim_cstr
std::string	claim_key
	The kept claim's key in the verdict table and skip set, and its row.
const goto_programt::instructiont *	claim_instruction = nullptr
	The instruction the kept claim was raised at.
property_locationt	claim_ploc
std::string	claim_property
std::string	claim_comment
	The kept claim's description and source position, for the property report.
locationt	claim_location
bool	claim_after_invariant_havoc = false
	Whether a –loop-invariant-check havoc step precedes the kept claim on this trace, so the claim is checked against the invariant's over-approximation rather than the program (issue #7480).
bool	show_slice_info
bool	is_goto_cov
namespacet	ns

Additional Inherited Members
Protected Attributes inherited from slicer
BigInt	sliced = 0
	tracks how many steps were sliced
Protected Attributes inherited from algorithm< symex_target_equationt::SSA_stepst >
const bool	sideeffect

Detailed Description

Claim slicer: remove every other claim of the formula with the exception of the one to keep.

Constructor & Destructor Documentation

claim_slicer()

claim_slicer::claim_slicer ( const size_t claim_to_keep, bool show_slice_info, bool is_goto_cov, namespacet & ns )

inlineexplicit

Member Function Documentation

run()

bool claim_slicer::run ( symex_target_equationt::SSA_stepst & )

overridevirtual

Executes the algorithm over a T object.

Returns

success of the algorithm

Implements algorithm< symex_target_equationt::SSA_stepst >.

Member Data Documentation

claim_after_invariant_havoc

bool claim_slicer::claim_after_invariant_havoc = false

Whether a –loop-invariant-check havoc step precedes the kept claim on this trace, so the claim is checked against the invariant's over-approximation rather than the program (issue #7480).

claim_comment

std::string claim_slicer::claim_comment

The kept claim's description and source position, for the property report.

claim_cstr

std::string claim_slicer::claim_cstr

claim_instruction

const goto_programt::instructiont* claim_slicer::claim_instruction = nullptr

The instruction the kept claim was raised at.

claim_key

std::string claim_slicer::claim_key

The kept claim's key in the verdict table and skip set, and its row.

Coverage goals keep claim_cstr, which their reports print.

claim_loc

std::string claim_slicer::claim_loc

claim_location

locationt claim_slicer::claim_location

claim_msg

std::string claim_slicer::claim_msg

claim_ploc

property_locationt claim_slicer::claim_ploc

claim_property

std::string claim_slicer::claim_property

claim_to_keep

size_t claim_slicer::claim_to_keep

is_goto_cov

bool claim_slicer::is_goto_cov

ns

namespacet claim_slicer::ns

show_slice_info

bool claim_slicer::show_slice_info

---

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

• src/goto-symex/equation/slice.h
• src/goto-symex/equation/slice.cpp