cprover
goto_statet Class Reference

Container for data that varies per program point, e.g. More...

#include <goto_state.h>

+ Inheritance diagram for goto_statet:
+ Collaboration diagram for goto_statet:

Public Member Functions

const symex_level2tget_level2 () const
 
void output_propagation_map (std::ostream &)
 Print the constant propagation map in a human-friendly format. More...
 
std::size_t complexity ()
 Get the complexity for this state. More...
 
 goto_statet ()=delete
 Constructors. More...
 
goto_statetoperator= (const goto_statet &other)=delete
 
goto_statetoperator= (goto_statet &&other)=default
 
 goto_statet (const goto_statet &other)=default
 
 goto_statet (goto_statet &&other)=default
 
 goto_statet (const class goto_symex_statet &s)
 
 goto_statet (guard_managert &guard_manager)
 
void apply_condition (const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
 Given a condition that must hold on this path, propagate as much knowledge as possible. More...
 

Public Attributes

unsigned depth = 0
 Distance from entry. More...
 
value_sett value_set
 Uses level 1 names, and is used to do dereferencing. More...
 
guardt guard
 
bool reachable
 Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual. More...
 
sharing_mapt< irep_idt, exprtpropagation
 
unsigned atomic_section_id = 0
 Threads. More...
 

Protected Attributes

symex_level2t level2
 

Detailed Description

Container for data that varies per program point, e.g.

the constant propagator state, when state needs to branch. This is copied out of goto_symex_statet at a control-flow fork and then back into it at a control-flow merge.

Definition at line 27 of file goto_state.h.

Constructor & Destructor Documentation

◆ goto_statet() [1/5]

goto_statet::goto_statet ( )
delete

Constructors.

◆ goto_statet() [2/5]

goto_statet::goto_statet ( const goto_statet other)
default

◆ goto_statet() [3/5]

goto_statet::goto_statet ( goto_statet &&  other)
default

◆ goto_statet() [4/5]

goto_statet::goto_statet ( const class goto_symex_statet s)
inlineexplicit

Definition at line 275 of file goto_symex_state.h.

◆ goto_statet() [5/5]

goto_statet::goto_statet ( guard_managert guard_manager)
inlineexplicit

Definition at line 88 of file goto_state.h.

Member Function Documentation

◆ apply_condition()

void goto_statet::apply_condition ( const exprt condition,
const goto_symex_statet previous_state,
const namespacet ns 
)

Given a condition that must hold on this path, propagate as much knowledge as possible.

For example, if the condition is (x == 5), whether that's an assumption or a GOTO condition that we just passed through, we can propagate the constant '5' for future 'x' references. If the condition is (y == &o1) then we can use that to populate the value set.

Parameters
conditioncondition that must hold on this path. Expected to already be L2-renamed.
previous_statecurrently active state, not necessarily the same as *this. For a GOTO instruction this is the state immediately preceding the branch while *this is the state that will be used on the taken- or not-taken path. For an ASSUME instruction previous_state and *this are equal.
nsglobal namespace

Definition at line 42 of file goto_state.cpp.

◆ complexity()

std::size_t goto_statet::complexity ( )
inline

Get the complexity for this state.

Used to short-circuit states if they have become too computationally complex.

Definition at line 72 of file goto_state.h.

◆ get_level2()

const symex_level2t& goto_statet::get_level2 ( ) const
inline

Definition at line 37 of file goto_state.h.

◆ operator=() [1/2]

goto_statet& goto_statet::operator= ( const goto_statet other)
delete

◆ operator=() [2/2]

goto_statet& goto_statet::operator= ( goto_statet &&  other)
default

◆ output_propagation_map()

void goto_statet::output_propagation_map ( std::ostream &  out)

Print the constant propagation map in a human-friendly format.

This is primarily for use from the debugger; please don't delete me just because there aren't any current callers.

Definition at line 18 of file goto_state.cpp.

Member Data Documentation

◆ atomic_section_id

unsigned goto_statet::atomic_section_id = 0

Threads.

Definition at line 68 of file goto_state.h.

◆ depth

unsigned goto_statet::depth = 0

Distance from entry.

Definition at line 31 of file goto_state.h.

◆ guard

guardt goto_statet::guard

Definition at line 50 of file goto_state.h.

◆ level2

symex_level2t goto_statet::level2
protected

Definition at line 34 of file goto_state.h.

◆ propagation

sharing_mapt<irep_idt, exprt> goto_statet::propagation

Definition at line 63 of file goto_state.h.

◆ reachable

bool goto_statet::reachable

Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual.

Definition at line 54 of file goto_state.h.

◆ value_set

value_sett goto_statet::value_set

Uses level 1 names, and is used to do dereferencing.

Definition at line 43 of file goto_state.h.


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