CBMC
goto_symex.cpp File Reference

Symbolic Execution. More...

#include "goto_symex.h"
#include "expr_skeleton.h"
#include "symex_assign.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/format_expr.h>
#include <util/fresh_symbol.h>
#include <util/mathematical_expr.h>
#include <util/mathematical_types.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/simplify_utils.h>
#include <util/std_code.h>
#include <util/string_expr.h>
#include <util/string_utils.h>
#include <climits>
+ Include dependency graph for goto_symex.cpp:

Go to the source code of this file.

Functions

static std::string get_alnum_string (const array_exprt &char_array)
 Maps the given array expression containing constant characters to a string containing only alphanumeric characters. More...
 

Detailed Description

Symbolic Execution.

Definition in file goto_symex.cpp.

Function Documentation

◆ get_alnum_string()

static std::string get_alnum_string ( const array_exprt char_array)
static

Maps the given array expression containing constant characters to a string containing only alphanumeric characters.

Parameters
char_arrayarray_exprt containing characters represented by expressions of kind constant_exprt and type unsignedbv_typet or signedbv_typet
Returns
a string containing only alphanumeric characters

Definition at line 152 of file goto_symex.cpp.