cprover
goto_symex_state.cpp File Reference

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>
Include dependency graph for goto_symex_state.cpp:

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)
 

Detailed Description

Symbolic Execution.

Definition in file goto_symex_state.cpp.

Function Documentation

§ assert_l1_renaming()

static void assert_l1_renaming ( const exprt expr)
static

Definition at line 299 of file goto_symex_state.cpp.

References check_renaming_l1(), and irept::pretty().

Referenced by goto_symex_statet::assignment().

§ assert_l2_renaming()

static void assert_l2_renaming ( const exprt expr)
static

Definition at line 312 of file goto_symex_state.cpp.

References check_renaming(), and irept::pretty().

Referenced by goto_symex_statet::assignment().

§ check_renaming() [1/2]

§ check_renaming() [2/2]

§ check_renaming_l1()

static bool check_renaming_l1 ( const exprt expr)
static