cprover
|
Symbolic Execution. More...
#include "goto_symex_state.h"
#include <cstdlib>
#include <cassert>
#include <iostream>
#include <util/base_exceptions.h>
#include <util/std_expr.h>
#include <util/prefix.h>
#include <analyses/dirty.h>
Go to the source code of this file.
Functions | |
static bool | check_renaming (const exprt &expr) |
write to a variable More... | |
static bool | check_renaming (const typet &type) |
static bool | check_renaming_l1 (const exprt &expr) |
static void | assert_l1_renaming (const exprt &expr) |
static void | assert_l2_renaming (const exprt &expr) |
Symbolic Execution.
Definition in file goto_symex_state.cpp.
|
static |
Definition at line 299 of file goto_symex_state.cpp.
References check_renaming_l1(), and irept::pretty().
Referenced by goto_symex_statet::assignment().
|
static |
Definition at line 312 of file goto_symex_state.cpp.
References check_renaming(), and irept::pretty().
Referenced by goto_symex_statet::assignment().
|
static |
write to a variable
Definition at line 268 of file goto_symex_state.cpp.
References check_renaming_l1(), forall_operands, irept::get_bool(), irept::id(), exprt::op0(), exprt::op1(), to_ssa_expr(), and exprt::type().
Referenced by assert_l2_renaming(), check_renaming(), and check_renaming_l1().
|
static |
Definition at line 220 of file goto_symex_state.cpp.
References check_renaming(), struct_union_typet::components(), typet::has_subtype(), irept::id(), array_typet::size(), typet::subtype(), to_array_type(), and to_struct_union_type().
|
static |
Definition at line 244 of file goto_symex_state.cpp.
References check_renaming(), forall_operands, irept::get_bool(), irept::id(), to_ssa_expr(), and exprt::type().
Referenced by assert_l1_renaming(), and check_renaming().