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.