frame_enforcer.cpp File Reference

Implementation of the observational frame rule. More...

#include "frame_enforcer.h"
#include <util/irep/migrate.h>
#include <util/irep/std_expr.h>
#include <util/lang/c_types.h>
#include <irep2/irep2_utils.h>

Include dependency graph for frame_enforcer.cpp:

Functions
static const expr2tc &	strip_typecasts (const expr2tc &e)
static bool	root_pointer_field (const expr2tc &e, irep_idt &ptr, irep_idt &field)
static void	emit_frame_instruction (goto_programt &dest, const locationt &loc, const expr2tc &guard, frame_modet mode, const std::string &var_name)
	Helper: emit a single ASSUME or ASSERT instruction with the given guard.
static void	emit_array_store_frame (goto_programt &dest, const locationt &loc, frame_modet mode, const std::vector< expr2tc > &assigned_indices, const expr2tc &var, const expr2tc &snap, const irep_idt &arr_name)
static void	emit_leaf_equalities (goto_programt &dest, const locationt &loc, frame_modet mode, const expr2tc &var_elem, const expr2tc &snap_elem, const expr2tc &exemption, const std::string &label)
static bool	emit_array_elem_frame (goto_programt &dest, const locationt &loc, frame_modet mode, const frame_enforcert::classified_assignst &classified, const expr2tc &var, const expr2tc &snap)
static bool	emit_struct_field_frame (goto_programt &dest, const locationt &loc, frame_modet mode, const frame_enforcert::classified_assignst &classified, const expr2tc &var, const expr2tc &snap)
static bool	emit_partial_frame (goto_programt &dest, const locationt &loc, frame_modet mode, const frame_enforcert::classified_assignst &classified, const expr2tc &var, const expr2tc &snap)
static bool	withhold_whole_object_frame (frame_modet mode, const frame_enforcert::classified_assignst &classified, const expr2tc &var)

Variables
static const unsigned	max_elementwise_frame_extent = 256

Detailed Description

Implementation of the observational frame rule.

This implements the core "Snapshot → Havoc/Call → Assume/Assert(Unchanged == Snapshot)" mechanism. See frame_enforcer.h for detailed documentation.

Function Documentation

emit_array_elem_frame()

bool emit_array_elem_frame ( goto_programt & dest, const locationt & loc, frame_modet mode, const frame_enforcert::classified_assignst & classified, const expr2tc & var, const expr2tc & snap )

static

emit_array_store_frame()

void emit_array_store_frame ( goto_programt & dest, const locationt & loc, frame_modet mode, const std::vector< expr2tc > & assigned_indices, const expr2tc & var, const expr2tc & snap, const irep_idt & arr_name )

static

emit_frame_instruction()

void emit_frame_instruction ( goto_programt & dest, const locationt & loc, const expr2tc & guard, frame_modet mode, const std::string & var_name )

static

Helper: emit a single ASSUME or ASSERT instruction with the given guard.

emit_leaf_equalities()

void emit_leaf_equalities ( goto_programt & dest, const locationt & loc, frame_modet mode, const expr2tc & var_elem, const expr2tc & snap_elem, const expr2tc & exemption, const std::string & label )

static

emit_partial_frame()

bool emit_partial_frame ( goto_programt & dest, const locationt & loc, frame_modet mode, const frame_enforcert::classified_assignst & classified, const expr2tc & var, const expr2tc & snap )

static

emit_struct_field_frame()

bool emit_struct_field_frame ( goto_programt & dest, const locationt & loc, frame_modet mode, const frame_enforcert::classified_assignst & classified, const expr2tc & var, const expr2tc & snap )

static

root_pointer_field()

bool root_pointer_field ( const expr2tc & e, irep_idt & ptr, irep_idt & field )

static

strip_typecasts()

const expr2tc & strip_typecasts ( const expr2tc & e )

static

withhold_whole_object_frame()

bool withhold_whole_object_frame ( frame_modet mode, const frame_enforcert::classified_assignst & classified, const expr2tc & var )

static

Variable Documentation

max_elementwise_frame_extent

const unsigned max_elementwise_frame_extent = 256

static