CBMC
|
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>
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... | |
Symbolic Execution.
Definition in file goto_symex.cpp.
|
static |
Maps the given array expression containing constant characters to a string containing only alphanumeric characters.
char_array | array_exprt containing characters represented by expressions of kind constant_exprt and type unsignedbv_typet or signedbv_typet |
Definition at line 152 of file goto_symex.cpp.