A class that generates instrumentation for assigns clause checking. More...

#include <instrument_spec_assigns.h>

Inheritance diagram for instrument_spec_assignst:

Collaboration diagram for instrument_spec_assignst:

Classes
class	location_intervalt
	Represents an interval of source locations covered by the static local variable search. More...

Public Member Functions
	instrument_spec_assignst (const irep_idt &_function_id, const goto_functionst &_functions, cfg_infot &_cfg_info, symbol_table_baset &_st, message_handlert &_message_handler)
	Class constructor. More...

void	track_spec_target (const exprt &expr, goto_programt &dest)
	Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in dest. More...

void	track_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest)
	Track a stack-allocated object and generate snaphsot instructions in dest. More...

bool	stack_allocated_is_tracked (const symbol_exprt &symbol_expr) const
	Returns true if the expression is tracked. More...

void	invalidate_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest)
	Generate instructions to invalidate a stack-allocated object that goes DEAD in dest. More...

void	track_heap_allocated (const exprt &expr, goto_programt &dest)
	Track a whole heap-alloc object and generate snaphsot instructions in dest. More...

void	track_static_locals (goto_programt &dest)
	Searches the goto instructions reachable from the start to the end of the instrumented function's instruction to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the `stack-allocated` set of tracked locations, and generates corresponding snapshot instructions in dest. More...

void	track_static_locals_between (goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)
	Searches the goto instructions reachable between the given `it` and `end` target instructions to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the `stack-allocated` set of tracked locations, and generates corresponding snapshot instructions in dest. More...

void	check_inclusion_assignment (const exprt &lhs, goto_programt &dest) const
	Generates inclusion check instructions for an assignment, havoc or havoc_object instruction. More...

void	check_inclusion_heap_allocated_and_invalidate_aliases (const exprt &expr, goto_programt &dest)
	Generates inclusion check instructions for an argument passed to free. More...

void	instrument_instructions (goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})
	Instruments a sequence of instructions with inclusion checks. More...

template<typename C >
void	get_static_locals (std::insert_iterator< C > inserter) const
	Inserts the detected static local symbols into a target container. More...

Protected Types
typedef std::unordered_map< irep_idt, location_intervalt >	covered_locationst
	Map type from function identifiers to covered locations. More...

typedef std::unordered_set< symbol_exprt, irep_hash >	propagated_static_localst

using	cond_target_exprt_to_car_mapt = std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash >

using	symbol_exprt_to_car_mapt = std::unordered_map< const symbol_exprt, const car_exprt, irep_hash >

using	exprt_to_car_mapt = std::unordered_map< const exprt, const car_exprt, irep_hash >

using	car_expr_listt = std::list< car_exprt >
	List of malloc'd conditional address ranges. More...

Protected Member Functions
void	traverse_instructions (const irep_idt ambient_function_id, goto_programt::const_targett it, const goto_programt::const_targett end, covered_locationst &covered_locations, propagated_static_localst &propagated) const
	Traverses the given list of instructions, updating the given coverage map, recursing into function calls only once. More...

void	collect_static_symbols (covered_locationst &covered_locations, std::unordered_set< symbol_exprt, irep_hash > &dest)
	Collects static symbols from the symbol table that have a source location included in one of the `covered_locations` and writes them into dest. More...

void	track_spec_target_group (const conditional_target_group_exprt &group, goto_programt &dest)
	Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause. More...

void	track_plain_spec_target (const exprt &expr, goto_programt &dest)
	Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause. More...

void	create_snapshot (const car_exprt &car, goto_programt &dest) const
	Returns snapshot instructions for a car_exprt. More...

exprt	target_validity_expr (const car_exprt &car, bool allow_null_target) const
	Returns the target validity expression for a car_exprt. More...

void	target_validity_assertion (const car_exprt &car, bool allow_null_target, goto_programt &dest) const
	Generates the target validity assertion for the given `car` and adds it to `dest`. More...

exprt	inclusion_check_single (const car_exprt &lhs, const car_exprt &candidate_car) const
	Returns inclusion check expression for a single candidate location. More...

exprt	inclusion_check_full (const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) const
	Returns an inclusion check expression of lhs over all tracked cars. More...

void	inclusion_check_assertion (const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) const
	Returns an inclusion check assertion of lhs over all tracked cars. More...

void	invalidate_car (const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const
	Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the same object as the freed car. More...

void	invalidate_heap_and_spec_aliases (const car_exprt &freed_car, goto_programt &dest) const
	Generates instructions to invalidate all targets aliased with a car that was passed to `free`, assuming the inclusion check passes, ie. More...

bool	must_track_decl (const goto_programt::const_targett &target) const
	Returns true iff a `DECL x` must be explicitly added to the write set. More...

bool	must_track_dead (const goto_programt::const_targett &target) const
	Returns true iff a `DEAD x` must be processed to update the write set. More...

bool	must_track_decl_or_dead (const irep_idt &ident) const
	Returns true iff a function-local symbol must be tracked. More...

bool	must_check_assign (const goto_programt::const_targett &target)
	Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented. More...

void	instrument_assign_statement (goto_programt::targett &instruction_it, goto_programt &body) const
	Inserts an assertion in `body` immediately before the assignment at `instruction_it`, to ensure that the LHS of the assignment is included in the set of currently tracked CARs. More...

void	instrument_call_statement (goto_programt::targett &instruction_it, goto_programt &body)
	Inserts an assertion in `body` immediately before the function call at `instruction_it`, to ensure that all memory locations written to by the called function are included in the set of currently tracked CARs. More...

const car_exprt &	create_car_from_spec_assigns (const exprt &condition, const exprt &target)

const car_exprt &	create_car_from_stack_alloc (const symbol_exprt &target)

const car_exprt &	create_car_from_heap_alloc (const exprt &target)

const car_exprt &	create_car_from_static_local (const symbol_exprt &target)

car_exprt	create_car_expr (const exprt &condition, const exprt &target) const
	Creates a conditional address range expression from a cleaned-up condition and target expression. More...

Protected Attributes
const irep_idt &	function_id
	Name of the instrumented function. More...

const goto_functionst &	functions
	Other functions of the model. More...

cfg_infot &	cfg_info
	CFG information for simplification. More...

symbol_table_baset &	st
	Program symbol table. More...

const namespacet	ns
	Program namespace. More...

messaget	log
	Logger. More...

const irep_idt &	mode
	Language mode. More...

cond_target_exprt_to_car_mapt	from_spec_assigns
	Map from conditional target expressions of assigns clauses to corresponding conditional address ranges. More...

symbol_exprt_to_car_mapt	from_stack_alloc
	Map from DECL symbols to corresponding conditional address ranges. More...

car_expr_listt	from_heap_alloc

symbol_exprt_to_car_mapt	from_static_local
	Map to from detected or propagated static local symbols to corresponding conditional address ranges. More...

Detailed Description

A class that generates instrumentation for assigns clause checking.

The track_* methods add targets to the sets of tracked targets and append instructions to the given destination program.

The check_inclusion_* methods generate assertions checking for inclusion of a designated target in one of the tracked targets, and append instructions to the given destination.

Definition at line 186 of file instrument_spec_assigns.h.

Member Typedef Documentation

◆ car_expr_listt

using instrument_spec_assignst::car_expr_listt = std::list<car_exprt>

protected

List of malloc'd conditional address ranges.

Definition at line 619 of file instrument_spec_assigns.h.

◆ cond_target_exprt_to_car_mapt

using instrument_spec_assignst::cond_target_exprt_to_car_mapt = std:: unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>

protected

Definition at line 597 of file instrument_spec_assigns.h.

◆ covered_locationst

typedef std::unordered_map<irep_idt, location_intervalt> instrument_spec_assignst::covered_locationst

protected

Map type from function identifiers to covered locations.

Definition at line 405 of file instrument_spec_assigns.h.

◆ exprt_to_car_mapt

using instrument_spec_assignst::exprt_to_car_mapt = std::unordered_map<const exprt, const car_exprt, irep_hash>

protected

Definition at line 615 of file instrument_spec_assigns.h.

◆ propagated_static_localst

typedef std::unordered_set<symbol_exprt, irep_hash> instrument_spec_assignst::propagated_static_localst

protected

Definition at line 406 of file instrument_spec_assigns.h.

◆ symbol_exprt_to_car_mapt

using instrument_spec_assignst::symbol_exprt_to_car_mapt = std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>

protected

Definition at line 607 of file instrument_spec_assigns.h.

Constructor & Destructor Documentation

◆ instrument_spec_assignst()

instrument_spec_assignst::instrument_spec_assignst	(	const irep_idt &	_function_id,
		const goto_functionst &	_functions,
		cfg_infot &	_cfg_info,
		symbol_table_baset &	_st,
		message_handlert &	_message_handler
	)

inline

Class constructor.

Parameters

_function_id	name of the instrumented function
_functions	other functions of the model
_cfg_info	control flow graph info about the function
_st	symbol table of the goto_model
_message_handler	used to output warning/error messages

Definition at line 196 of file instrument_spec_assigns.h.

Member Function Documentation

◆ check_inclusion_assignment()

void instrument_spec_assignst::check_inclusion_assignment	(	const exprt &	lhs,
		goto_programt &	dest
	)		const

Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.

Parameters

lhs	the assignment lhs or argument to havoc/havoc_object
dest	destination program to append instructions to

Definition at line 146 of file instrument_spec_assigns.cpp.

◆ check_inclusion_heap_allocated_and_invalidate_aliases()

void instrument_spec_assignst::check_inclusion_heap_allocated_and_invalidate_aliases	(	const exprt &	expr,
		goto_programt &	dest
	)

Generates inclusion check instructions for an argument passed to free.

Parameters

expr	the argument to the free operator
dest	destination program to append instructions to

Definition at line 304 of file instrument_spec_assigns.cpp.

◆ collect_static_symbols()

void instrument_spec_assignst::collect_static_symbols	(	covered_locationst &	covered_locations,
		std::unordered_set< symbol_exprt, irep_hash > &	dest
	)

protected

Collects static symbols from the symbol table that have a source location included in one of the covered_locations and writes them into dest.

Definition at line 284 of file instrument_spec_assigns.cpp.

◆ create_car_expr()

car_exprt instrument_spec_assignst::create_car_expr	(	const exprt &	condition,
		const exprt &	target
	)		const

protected

Creates a conditional address range expression from a cleaned-up condition and target expression.

Definition at line 464 of file instrument_spec_assigns.cpp.

◆ create_car_from_heap_alloc()

const car_exprt & instrument_spec_assignst::create_car_from_heap_alloc ( const exprt & target )

protected

Definition at line 865 of file instrument_spec_assigns.cpp.

◆ create_car_from_spec_assigns()

const car_exprt & instrument_spec_assignst::create_car_from_spec_assigns	(	const exprt &	condition,
		const exprt &	target
	)

protected

Definition at line 821 of file instrument_spec_assigns.cpp.

◆ create_car_from_stack_alloc()

const car_exprt & instrument_spec_assignst::create_car_from_stack_alloc ( const symbol_exprt & target )

protected

Definition at line 844 of file instrument_spec_assigns.cpp.

◆ create_car_from_static_local()

const car_exprt & instrument_spec_assignst::create_car_from_static_local ( const symbol_exprt & target )

protected

Definition at line 873 of file instrument_spec_assigns.cpp.

◆ create_snapshot()

void instrument_spec_assignst::create_snapshot	(	const car_exprt &	car,
		goto_programt &	dest
	)		const

protected

Returns snapshot instructions for a car_exprt.

Definition at line 606 of file instrument_spec_assigns.cpp.

◆ get_static_locals()

template<typename C >

void instrument_spec_assignst::get_static_locals ( std::insert_iterator< C > inserter ) const

inline

Inserts the detected static local symbols into a target container.

Template Parameters

C	The type of the target container

Parameters

inserter An insert_iterator on the target container

Definition at line 462 of file instrument_spec_assigns.h.

◆ inclusion_check_assertion()

void instrument_spec_assignst::inclusion_check_assertion	(	const car_exprt &	lhs,
		bool	allow_null_lhs,
		bool	include_stack_allocated,
		goto_programt &	dest
	)		const

protected

Returns an inclusion check assertion of lhs over all tracked cars.

Parameters

lhs	the lhs expression to check for inclusion
allow_null_lhs	if true, allow the lhs to be NULL
include_stack_allocated	if true, include stack allocated targets in the inclusion check.
dest	destination program to append instructions to

Definition at line 688 of file instrument_spec_assigns.cpp.

◆ inclusion_check_full()

exprt instrument_spec_assignst::inclusion_check_full	(	const car_exprt &	lhs,
		bool	allow_null_lhs,
		bool	include_stack_allocated
	)		const

protected

Returns an inclusion check expression of lhs over all tracked cars.

Parameters

lhs	the lhs expression to check for inclusion
allow_null_lhs	if true, allow the lhs to be NULL
include_stack_allocated	if true, include stack allocated targets in the inclusion check.

Definition at line 749 of file instrument_spec_assigns.cpp.

◆ inclusion_check_single()

exprt instrument_spec_assignst::inclusion_check_single	(	const car_exprt &	lhs,
		const car_exprt &	candidate_car
	)		const

protected

Returns inclusion check expression for a single candidate location.

Definition at line 730 of file instrument_spec_assigns.cpp.

◆ instrument_assign_statement()

void instrument_spec_assignst::instrument_assign_statement	(	goto_programt::targett &	instruction_it,
		goto_programt &	body
	)		const

protected

Inserts an assertion in body immediately before the assignment at instruction_it, to ensure that the LHS of the assignment is included in the set of currently tracked CARs.

Definition at line 1018 of file instrument_spec_assigns.cpp.

◆ instrument_call_statement()

void instrument_spec_assignst::instrument_call_statement	(	goto_programt::targett &	instruction_it,
		goto_programt &	body
	)

protected

Inserts an assertion in body immediately before the function call at instruction_it, to ensure that all memory locations written to by the called function are included in the set of currently tracked CARs.

Definition at line 1029 of file instrument_spec_assigns.cpp.

◆ instrument_instructions()

void instrument_spec_assignst::instrument_instructions	(	goto_programt &	body,
		goto_programt::targett	instruction_it,
		const goto_programt::targett &	instruction_end,
		const std::function< bool(const goto_programt::targett &)> &	pred = `{}`
	)

Instruments a sequence of instructions with inclusion checks.

If pred is not provided, then all instructions are instrumented. If pred is provided, then only the instructions that satisfy pred are instrumented.

Parameters

body	goto program containing the instructions
instruction_it	target to the first instruction of the sequence
instruction_end	target to the last instruction of the sequence
pred	a predicate on targets to check if they should be instrumented

Definition at line 323 of file instrument_spec_assigns.cpp.

◆ invalidate_car()

void instrument_spec_assignst::invalidate_car	(	const car_exprt &	tracked_car,
		const car_exprt &	freed_car,
		goto_programt &	result
	)		const

protected

Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the same object as the freed car.

Definition at line 893 of file instrument_spec_assigns.cpp.

◆ invalidate_heap_and_spec_aliases()

void instrument_spec_assignst::invalidate_heap_and_spec_aliases	(	const car_exprt &	freed_car,
		goto_programt &	dest
	)		const

protected

Generates instructions to invalidate all targets aliased with a car that was passed to free, assuming the inclusion check passes, ie.

that the freed_car is fully included in one of the tracked targets.

Definition at line 910 of file instrument_spec_assigns.cpp.

◆ invalidate_stack_allocated()

void instrument_spec_assignst::invalidate_stack_allocated	(	const symbol_exprt &	symbol_expr,
		goto_programt &	dest
	)

Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.

Definition at line 113 of file instrument_spec_assigns.cpp.

◆ must_check_assign()

bool instrument_spec_assignst::must_check_assign ( const goto_programt::const_targett & target )

protected

Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.

Definition at line 922 of file instrument_spec_assigns.cpp.

◆ must_track_dead()

bool instrument_spec_assignst::must_track_dead ( const goto_programt::const_targett & target ) const

protected

Returns true iff a DEAD x must be processed to update the write set.

Returns true iff a DEAD x must be processed to upate the local write set.

See also: must_track_decl_or_dead.

The conditions are the same than for tracking a DECL x instruction.

Definition at line 1012 of file instrument_spec_assigns.cpp.

◆ must_track_decl()

bool instrument_spec_assignst::must_track_decl ( const goto_programt::const_targett & target ) const

protected

Returns true iff a DECL x must be explicitly added to the write set.

Returns true iff a DECL x must be explicitly tracked in the write set.

See also: must_track_decl_or_dead.

Definition at line 990 of file instrument_spec_assigns.cpp.

◆ must_track_decl_or_dead()

bool instrument_spec_assignst::must_track_decl_or_dead ( const irep_idt & ident ) const

protected

Returns true iff a function-local symbol must be tracked.

Track the symbol is not a local or is a dirty local.

A local is called 'dirty' if its address gets taken at some point in the program.

Assuming the goto program is obtained from a structured C program that passed C compiler checks, non-dirty locals can only be assigned to directly by name, cannot escape their lexical scope, and are always safe to assign. Hence, we only track dirty locals in the write set.

Definition at line 983 of file instrument_spec_assigns.cpp.

◆ stack_allocated_is_tracked()

bool instrument_spec_assignst::stack_allocated_is_tracked ( const symbol_exprt & symbol_expr ) const

Returns true if the expression is tracked.

Definition at line 107 of file instrument_spec_assigns.cpp.

◆ target_validity_assertion()

void instrument_spec_assignst::target_validity_assertion	(	const car_exprt &	car,
		bool	allow_null_target,
		goto_programt &	dest
	)		const

protected

Generates the target validity assertion for the given car and adds it to dest.

The assertion checks that if the car's condition holds then the target is r_ok (or NULL if allow_null_targets is true).

Definition at line 657 of file instrument_spec_assigns.cpp.

◆ target_validity_expr()

exprt instrument_spec_assignst::target_validity_expr	(	const car_exprt &	car,
		bool	allow_null_target
	)		const

protected

Returns the target validity expression for a car_exprt.

Definition at line 638 of file instrument_spec_assigns.cpp.

◆ track_heap_allocated()

void instrument_spec_assignst::track_heap_allocated	(	const exprt &	expr,
		goto_programt &	dest
	)

Track a whole heap-alloc object and generate snaphsot instructions in dest.

Definition at line 132 of file instrument_spec_assigns.cpp.

◆ track_plain_spec_target()

void instrument_spec_assignst::track_plain_spec_target	(	const exprt &	expr,
		goto_programt &	dest
	)

protected

Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause.

Definition at line 431 of file instrument_spec_assigns.cpp.

◆ track_spec_target()

void instrument_spec_assignst::track_spec_target	(	const exprt &	expr,
		goto_programt &	dest
	)

Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in dest.

Definition at line 90 of file instrument_spec_assigns.cpp.

◆ track_spec_target_group()

void instrument_spec_assignst::track_spec_target_group	(	const conditional_target_group_exprt &	group,
		goto_programt &	dest
	)

protected

Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause.

Definition at line 407 of file instrument_spec_assigns.cpp.

◆ track_stack_allocated()

void instrument_spec_assignst::track_stack_allocated	(	const symbol_exprt &	symbol_expr,
		goto_programt &	dest
	)

Track a stack-allocated object and generate snaphsot instructions in dest.

Definition at line 100 of file instrument_spec_assigns.cpp.

◆ track_static_locals()

void instrument_spec_assignst::track_static_locals ( goto_programt & dest )

Searches the goto instructions reachable from the start to the end of the instrumented function's instruction to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest.

Parameters

dest	a snaphot program for the identified static locals.

Definition at line 156 of file instrument_spec_assigns.cpp.

◆ track_static_locals_between()

void instrument_spec_assignst::track_static_locals_between	(	goto_programt::const_targett	it,
		const goto_programt::const_targett	end,
		goto_programt &	dest
	)

Searches the goto instructions reachable between the given it and end target instructions to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest.

Parameters

it	start instruction (inclusive)
end	end instruction (exclusive)
dest	a snaphot program for the identified static locals.

Definition at line 184 of file instrument_spec_assigns.cpp.

◆ traverse_instructions()

void instrument_spec_assignst::traverse_instructions	(	const irep_idt	ambient_function_id,
		goto_programt::const_targett	it,
		const goto_programt::const_targett	end,
		covered_locationst &	covered_locations,
		propagated_static_localst &	propagated
	)		const

protected

Traverses the given list of instructions, updating the given coverage map, recursing into function calls only once.

When the traversal terminates, the map will contain one entry per visited function, with the associated range of locations covered by the traversal. Function names and line numbers are collected from source locations attached to the instructions.

Definition at line 203 of file instrument_spec_assigns.cpp.

Member Data Documentation

◆ cfg_info

cfg_infot& instrument_spec_assignst::cfg_info

protected

CFG information for simplification.

Definition at line 480 of file instrument_spec_assigns.h.

◆ from_heap_alloc

car_expr_listt instrument_spec_assignst::from_heap_alloc

protected

Definition at line 620 of file instrument_spec_assigns.h.

◆ from_spec_assigns

cond_target_exprt_to_car_mapt instrument_spec_assignst::from_spec_assigns

protected

Map from conditional target expressions of assigns clauses to corresponding conditional address ranges.

Definition at line 602 of file instrument_spec_assigns.h.

◆ from_stack_alloc

symbol_exprt_to_car_mapt instrument_spec_assignst::from_stack_alloc

protected

Map from DECL symbols to corresponding conditional address ranges.

Definition at line 611 of file instrument_spec_assigns.h.

◆ from_static_local

symbol_exprt_to_car_mapt instrument_spec_assignst::from_static_local

protected

Map to from detected or propagated static local symbols to corresponding conditional address ranges.

Definition at line 626 of file instrument_spec_assigns.h.

◆ function_id

const irep_idt& instrument_spec_assignst::function_id

protected

Name of the instrumented function.

Definition at line 474 of file instrument_spec_assigns.h.

◆ functions

const goto_functionst& instrument_spec_assignst::functions

protected

Other functions of the model.

Definition at line 477 of file instrument_spec_assigns.h.

◆ log

messaget instrument_spec_assignst::log

protected

Logger.

Definition at line 489 of file instrument_spec_assigns.h.

◆ mode

const irep_idt& instrument_spec_assignst::mode

protected

Language mode.

Definition at line 492 of file instrument_spec_assigns.h.

◆ ns

const namespacet instrument_spec_assignst::ns

protected

Program namespace.

Definition at line 486 of file instrument_spec_assigns.h.

◆ st

symbol_table_baset& instrument_spec_assignst::st

protected

Program symbol table.

Definition at line 483 of file instrument_spec_assigns.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/instrument_spec_assigns.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/instrument_spec_assigns.cpp

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ car_expr_listt

◆ cond_target_exprt_to_car_mapt

◆ covered_locationst

◆ exprt_to_car_mapt

◆ propagated_static_localst

◆ symbol_exprt_to_car_mapt

Constructor & Destructor Documentation

◆ instrument_spec_assignst()

Member Function Documentation

◆ check_inclusion_assignment()

◆ check_inclusion_heap_allocated_and_invalidate_aliases()

◆ collect_static_symbols()

◆ create_car_expr()

◆ create_car_from_heap_alloc()

◆ create_car_from_spec_assigns()

◆ create_car_from_stack_alloc()

◆ create_car_from_static_local()

◆ create_snapshot()

◆ get_static_locals()

◆ inclusion_check_assertion()

◆ inclusion_check_full()

◆ inclusion_check_single()

◆ instrument_assign_statement()

◆ instrument_call_statement()

◆ instrument_instructions()

◆ invalidate_car()

◆ invalidate_heap_and_spec_aliases()

◆ invalidate_stack_allocated()

◆ must_check_assign()

◆ must_track_dead()

◆ must_track_decl()

◆ must_track_decl_or_dead()

◆ stack_allocated_is_tracked()

◆ target_validity_assertion()

◆ target_validity_expr()

◆ track_heap_allocated()

◆ track_plain_spec_target()

◆ track_spec_target()

◆ track_spec_target_group()

◆ track_stack_allocated()

◆ track_static_locals()

◆ track_static_locals_between()

◆ traverse_instructions()

Member Data Documentation

◆ cfg_info

◆ from_heap_alloc

◆ from_spec_assigns

◆ from_stack_alloc

◆ from_static_local

◆ function_id

◆ functions

◆ log

◆ mode

◆ ns

◆ st