cprover
goto_symex_state.cpp File Reference
#include "goto_symex_state.h"
#include <cstdlib>
#include <iostream>
#include <util/base_exceptions.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/format.h>
#include <util/format_expr.h>
#include <util/invariant.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <analyses/dirty.h>
+ Include dependency graph for goto_symex_state.cpp:

Go to the source code of this file.

Classes

class  goto_symex_is_constantt
 

Functions

static void get_l1_name (exprt &expr)
 
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)
 

Detailed Description

Symbolic Execution

Definition in file goto_symex_state.cpp.

Function Documentation

◆ check_renaming() [1/2]

static bool check_renaming ( const exprt expr)
static

write to a variable

Definition at line 90 of file goto_symex_state.cpp.

◆ check_renaming() [2/2]

static bool check_renaming ( const typet type)
static

Definition at line 48 of file goto_symex_state.cpp.

◆ check_renaming_l1()

static bool check_renaming_l1 ( const exprt expr)
static

Definition at line 66 of file goto_symex_state.cpp.

◆ get_l1_name()

static void get_l1_name ( exprt expr)
static

Definition at line 755 of file goto_symex_state.cpp.