Loading...

Searching...

No Matches

goto_symex.cpp File Reference

Symbolic Execution. More...

#include "goto_symex.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_utils.h>
#include <util/std_code.h>
#include <util/string_expr.h>
#include <util/string_utils.h>
#include "expr_skeleton.h"
#include "simplify_expr_with_value_set.h"
#include "symex_assign.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.

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_array array_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 166 of file goto_symex.cpp.