CBMC: /home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement_util.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

string_refinement_util.h File Reference

#include "string_constraint.h"
#include <map>
#include <set>

+ Include dependency graph for string_refinement_util.h:

+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct index_set_pairt

struct string_axiomst

class sparse_arrayt

Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list of entries (i,a), (j,b) etc. More...

class interval_sparse_arrayt

Represents arrays by the indexes up to which the value remains the same. More...

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.