Loading...

Searching...

No Matches

string_refinement_util.cpp File Reference

#include "string_refinement_util.h"
#include <numeric>
#include <util/arith_tools.h>
#include <util/expr_util.h>
#include <util/magic.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/unicode.h>

+ Include dependency graph for string_refinement_util.cpp:

[フレーム]

Go to the source code of this file.

Functions

bool is_char_type (const typet &type)

For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.

bool is_char_array_type (const typet &type, const namespacet &ns)

Distinguish char array from other types.

bool is_char_pointer_type (const typet &type)

For now, any unsigned bitvector type is considered a character.

bool has_char_pointer_subtype (const typet &type, const namespacet &ns)

bool has_char_array_subexpr (const exprt &expr, const namespacet &ns)

std::string utf16_constant_array_to_java (const array_exprt &arr, std::size_t length)

Construct a string from a constant array.

Function Documentation

◆ has_char_array_subexpr()

bool has_char_array_subexpr ( const exprt & expr,

const namespacet & ns

)

Parameters: expr an expression

ns namespace

Returns: true if a subexpression of expr is an array of characters

Definition at line 45 of file string_refinement_util.cpp.

◆ has_char_pointer_subtype()

bool has_char_pointer_subtype ( const typet & type,

const namespacet & ns

)

Parameters: type a type

ns namespace

Returns: true if a subtype of type is an pointer of characters. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc...

Definition at line 40 of file string_refinement_util.cpp.

◆ is_char_array_type()

bool is_char_array_type ( const typet & type,

const namespacet & ns

)

Distinguish char array from other types.

For now, any unsigned bitvector type is considered a character.

Parameters: type a type

ns namespace

Returns: true if the given type is an array of characters

Definition at line 26 of file string_refinement_util.cpp.

◆ is_char_pointer_type()

bool is_char_pointer_type ( const typet & type )

For now, any unsigned bitvector type is considered a character.

Parameters: type a type

Returns: true if the given type represents a pointer to characters

Definition at line 34 of file string_refinement_util.cpp.

◆ is_char_type()

bool is_char_type ( const typet & type )

For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.

Note: type that are not characters maybe detected as characters (for instance unsigned char in C), this will make dec_solve do unnecessary steps for these, but should not affect correctness.

Parameters: type a type

Returns: true if the given type represents characters

Definition at line 20 of file string_refinement_util.cpp.

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java ( const array_exprt & arr,

std::size_t length

)

Construct a string from a constant array.

Parameters: arr an array expression containing only constants

length an unsigned value representing the length of the array

Returns: String of length length represented by the array assuming each field in arr represents a character.

Definition at line 52 of file string_refinement_util.cpp.