cprover
|
Single SSA step in the equation. More...
#include <symex_target_equation.h>
Public Member Functions | |
bool | is_assert () const |
bool | is_assume () const |
bool | is_assignment () const |
bool | is_goto () const |
bool | is_constraint () const |
bool | is_location () const |
bool | is_output () const |
bool | is_decl () const |
bool | is_function_call () const |
bool | is_function_return () const |
bool | is_shared_read () const |
bool | is_shared_write () const |
bool | is_spawn () const |
bool | is_memory_barrier () const |
bool | is_atomic_begin () const |
bool | is_atomic_end () const |
SSA_stept () | |
void | output (const namespacet &ns, std::ostream &out) const |
void | output (std::ostream &out) const |
void | validate (const namespacet &ns, const validation_modet vm) const |
Check that the SSA step is well-formed. More... | |
Public Attributes | |
sourcet | source |
goto_trace_stept::typet | type |
bool | hidden =false |
exprt | guard |
literalt | guard_literal |
ssa_exprt | ssa_lhs |
exprt | ssa_full_lhs |
exprt | original_full_lhs |
exprt | ssa_rhs |
assignment_typet | assignment_type |
exprt | cond_expr |
literalt | cond_literal |
std::string | comment |
irep_idt | format_string |
irep_idt | io_id |
bool | formatted =false |
std::list< exprt > | io_args |
std::list< exprt > | converted_io_args |
irep_idt | called_function |
std::vector< exprt > | ssa_function_arguments |
std::vector< exprt > | converted_function_arguments |
unsigned | atomic_section_id =0 |
bool | ignore =false |
Single SSA step in the equation.
Its type
is defined as goto_trace_stept::typet. Every SSA step has a source
to identify its origin in the input GOTO program and a guard
expression which holds the path condition required to reach this step: they limit the scope of this step.
SSA steps that represent assignments and declarations also store the left- and right-hand sides of the assignment. The left-hand side ssa_lhs
is required to be of type ssa_exprt: in SSA form, variables are only assigned once, see Static Single Assignment (SSA) Form. To achieve that, we annotate the original name with 3 types of levels, see ssa_exprt. The assignment step also represents the left-hand side in two other full forms: ssa_full_lhs
and original_full_lhs
, which store the original expressions from the input GOTO program before removing array indexes, pointers, etc. The ssa_full_lhs
uses the level-annotated names.
Assumptions, assertions, goto steps, and constraints have cond_expr
which represent the condition guarding this step, i.e. what must hold for this step to be taken. Both guard
and cond_expr
will later be translated into verification condition for the SAT/SMT solver (or some other decision procedure), to be referred by their respective literals. Constraints usually arise from external conditions, such as memory models or partial orders: they represent assumptions with global effect.
Function calls store called_function
name as well as a vector of arguments ssa_function_arguments
. The converted
version of a variable will contain its version for the SAT/SMT conversion.
Definition at line 243 of file symex_target_equation.h.
|
inline |
Definition at line 318 of file symex_target_equation.h.
|
inline |
Definition at line 250 of file symex_target_equation.h.
|
inline |
Definition at line 254 of file symex_target_equation.h.
|
inline |
Definition at line 252 of file symex_target_equation.h.
|
inline |
Definition at line 278 of file symex_target_equation.h.
|
inline |
Definition at line 280 of file symex_target_equation.h.
|
inline |
Definition at line 258 of file symex_target_equation.h.
|
inline |
Definition at line 264 of file symex_target_equation.h.
|
inline |
Definition at line 266 of file symex_target_equation.h.
|
inline |
Definition at line 268 of file symex_target_equation.h.
|
inline |
Definition at line 256 of file symex_target_equation.h.
|
inline |
Definition at line 260 of file symex_target_equation.h.
|
inline |
Definition at line 276 of file symex_target_equation.h.
|
inline |
Definition at line 262 of file symex_target_equation.h.
|
inline |
Definition at line 270 of file symex_target_equation.h.
|
inline |
Definition at line 272 of file symex_target_equation.h.
|
inline |
Definition at line 274 of file symex_target_equation.h.
void symex_target_equationt::SSA_stept::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 729 of file symex_target_equation.cpp.
void symex_target_equationt::SSA_stept::output | ( | std::ostream & | out | ) | const |
Definition at line 832 of file symex_target_equation.cpp.
void symex_target_equationt::SSA_stept::validate | ( | const namespacet & | ns, |
const validation_modet | vm | ||
) | const |
Check that the SSA step is well-formed.
ns | namespace to lookup identifiers |
vm | validation mode to be used for reporting failures |
Definition at line 950 of file symex_target_equation.cpp.
assignment_typet symex_target_equationt::SSA_stept::assignment_type |
Definition at line 292 of file symex_target_equation.h.
unsigned symex_target_equationt::SSA_stept::atomic_section_id =0 |
Definition at line 313 of file symex_target_equation.h.
irep_idt symex_target_equationt::SSA_stept::called_function |
Definition at line 306 of file symex_target_equation.h.
std::string symex_target_equationt::SSA_stept::comment |
Definition at line 297 of file symex_target_equation.h.
exprt symex_target_equationt::SSA_stept::cond_expr |
Definition at line 295 of file symex_target_equation.h.
literalt symex_target_equationt::SSA_stept::cond_literal |
Definition at line 296 of file symex_target_equation.h.
std::vector<exprt> symex_target_equationt::SSA_stept::converted_function_arguments |
Definition at line 309 of file symex_target_equation.h.
std::list<exprt> symex_target_equationt::SSA_stept::converted_io_args |
Definition at line 303 of file symex_target_equation.h.
irep_idt symex_target_equationt::SSA_stept::format_string |
Definition at line 300 of file symex_target_equation.h.
bool symex_target_equationt::SSA_stept::formatted =false |
Definition at line 301 of file symex_target_equation.h.
exprt symex_target_equationt::SSA_stept::guard |
Definition at line 285 of file symex_target_equation.h.
literalt symex_target_equationt::SSA_stept::guard_literal |
Definition at line 286 of file symex_target_equation.h.
bool symex_target_equationt::SSA_stept::hidden =false |
Definition at line 283 of file symex_target_equation.h.
bool symex_target_equationt::SSA_stept::ignore =false |
Definition at line 316 of file symex_target_equation.h.
std::list<exprt> symex_target_equationt::SSA_stept::io_args |
Definition at line 302 of file symex_target_equation.h.
irep_idt symex_target_equationt::SSA_stept::io_id |
Definition at line 300 of file symex_target_equation.h.
exprt symex_target_equationt::SSA_stept::original_full_lhs |
Definition at line 290 of file symex_target_equation.h.
sourcet symex_target_equationt::SSA_stept::source |
Definition at line 246 of file symex_target_equation.h.
exprt symex_target_equationt::SSA_stept::ssa_full_lhs |
Definition at line 290 of file symex_target_equation.h.
std::vector<exprt> symex_target_equationt::SSA_stept::ssa_function_arguments |
Definition at line 309 of file symex_target_equation.h.
ssa_exprt symex_target_equationt::SSA_stept::ssa_lhs |
Definition at line 289 of file symex_target_equation.h.
exprt symex_target_equationt::SSA_stept::ssa_rhs |
Definition at line 291 of file symex_target_equation.h.
goto_trace_stept::typet symex_target_equationt::SSA_stept::type |
Definition at line 247 of file symex_target_equation.h.