write_stack_entryt Class Reference

#include <write_stack_entry.h>

Inheritance diagram for write_stack_entryt:

Public Member Functions
virtual	~write_stack_entryt ()=default
virtual std::pair< exprt, bool >	get_access_expr () const =0
virtual bool	try_squash_in (std::shared_ptr< const write_stack_entryt > new_entry, const abstract_environmentt &enviroment, const namespacet &ns)
	Try to combine a new stack element with the current top of the stack. More...

Detailed Description

Definition at line 20 of file write_stack_entry.h.

Constructor & Destructor Documentation

~write_stack_entryt()

virtual write_stack_entryt::~write_stack_entryt ( )

virtualdefault

Member Function Documentation

get_access_expr()

virtual std::pair<exprt, bool> write_stack_entryt::get_access_expr ( ) const

pure virtual

Implemented in offset_entryt, and simple_entryt.

try_squash_in()

bool write_stack_entryt::try_squash_in ( std::shared_ptr< const write_stack_entryt >  new_entry, const abstract_environmentt &  enviroment, const namespacet &  ns  )

virtual

Try to combine a new stack element with the current top of the stack.

Parameters

new_entry	The new entry to combine with
enviroment	The enviroment to evalaute things in
ns	The global namespace

Returns

True if this stack entry and thew new entry were combined

Reimplemented in offset_entryt.

Definition at line 22 of file write_stack_entry.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/write_stack_entry.h
• /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/write_stack_entry.cpp