string_constraint_generatort Class Reference

#include <string_constraint_generator.h>

Collaboration diagram for string_constraint_generatort:

Classes
struct	parseint_argumentst
	Argument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt. More...

Public Member Functions
	string_constraint_generatort (const namespacet &ns, message_handlert &message_handler)
std::pair< exprt, string_constraintst >	add_axioms_for_function_application (const function_application_exprt &expr)
	strings contained in this call are converted to objects of type string_exprt, through adding axioms. More...
std::optional< exprt >	make_array_pointer_association (const exprt &return_code, const function_application_exprt &expr)
	Associate array to pointer, and array to length. More...
std::pair< exprt, string_constraintst >	add_axioms_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
	Add axioms enforcing that res is equal to the concatenation of s1 and s2. More...
std::pair< exprt, string_constraintst >	add_axioms_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
	Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at indexend_index'‘. More...
std::pair< exprt, string_constraintst >	add_axioms_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
std::pair< exprt, string_constraintst >	add_axioms_for_string_of_int_with_radix (const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size)
	Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression. More...
string_constraintst	add_constraint_on_characters (const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
	Add constraint on characters of a string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_constrain_characters (const function_application_exprt &f)
	Add axioms to ensure all characters of a string belong to a given set. More...
std::pair< exprt, string_constraintst >	add_axioms_for_char_at (const function_application_exprt &f)
	Character at a given position. More...
std::pair< exprt, string_constraintst >	add_axioms_for_code_point_at (const function_application_exprt &f)
	add axioms corresponding to the String.codePointAt java function More...
std::pair< exprt, string_constraintst >	add_axioms_for_code_point_before (const function_application_exprt &f)
	add axioms corresponding to the String.codePointBefore java function More...
std::pair< exprt, string_constraintst >	add_axioms_for_contains (const function_application_exprt &f)
	Test whether a string contains another. More...
std::pair< exprt, string_constraintst >	add_axioms_for_equals (const function_application_exprt &f)
	Equality of the content of two strings. More...
std::pair< exprt, string_constraintst >	add_axioms_for_equals_ignore_case (const function_application_exprt &f)
	Equality of the content ignoring case of characters. More...
std::pair< exprt, string_constraintst >	add_axioms_for_is_empty (const function_application_exprt &f)
	Add axioms stating that the returned value is true exactly when the argument string is empty. More...
std::pair< exprt, string_constraintst >	add_axioms_for_is_prefix (const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
	Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset. More...
std::pair< exprt, string_constraintst >	add_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments)
	Test if the target is a prefix of the string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_is_suffix (const function_application_exprt &f, bool swap_arguments)
	Test if the target is a suffix of the string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_length (const function_application_exprt &f)
	Length of a string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_empty_string (const function_application_exprt &f)
	Add axioms to say that the returned string expression is empty. More...
std::pair< exprt, string_constraintst >	add_axioms_for_copy (const function_application_exprt &f)
	add axioms to say that the returned string expression is equal to the argument of the function application More...
std::pair< exprt, string_constraintst >	add_axioms_for_concat_code_point (const function_application_exprt &f)
	Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More...
std::pair< exprt, string_constraintst >	add_axioms_for_constant (const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
	Add axioms ensuring that the provided string expression and constant are equal. More...
std::pair< exprt, string_constraintst >	add_axioms_for_delete (const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
	Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). More...
std::pair< exprt, string_constraintst >	add_axioms_for_delete (const function_application_exprt &f)
	Remove a portion of a string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_delete_char_at (const function_application_exprt &expr)
	add axioms corresponding to the StringBuilder.deleteCharAt java function More...
std::pair< exprt, string_constraintst >	add_axioms_for_cprover_string (const array_string_exprt &res, const exprt &arg, const exprt &guard)
	Convert an expression of type string_typet to a string_exprt. More...
std::pair< exprt, string_constraintst >	add_axioms_from_literal (const function_application_exprt &f)
	String corresponding to an internal cprover string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_string_of_int (const array_string_exprt &res, const exprt &input_int, size_t max_size)
	Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression. More...
std::pair< exprt, string_constraintst >	add_axioms_from_int_hex (const array_string_exprt &res, const exprt &i)
	Add axioms stating that the string res corresponds to the integer argument written in hexadecimal. More...
std::pair< exprt, string_constraintst >	add_axioms_from_int_hex (const function_application_exprt &f)
	Add axioms corresponding to the Integer.toHexString(I) java function. More...
std::pair< exprt, string_constraintst >	add_axioms_from_long (const function_application_exprt &f)
	Add axioms corresponding to the String.valueOf(J) java function. More...
std::pair< exprt, string_constraintst >	add_axioms_from_bool (const function_application_exprt &f)
std::pair< exprt, string_constraintst >	add_axioms_from_bool (const array_string_exprt &res, const exprt &b)
	Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false. More...
std::pair< exprt, string_constraintst >	add_axioms_from_char (const function_application_exprt &f)
std::pair< exprt, string_constraintst >	add_axioms_from_char (const array_string_exprt &res, const exprt &c)
std::pair< exprt, string_constraintst >	add_axioms_for_index_of (const array_string_exprt &str, const exprt &c, const exprt &from_index)
	Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. More...
std::pair< exprt, string_constraintst >	add_axioms_for_index_of_string (const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
	Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. More...
std::pair< exprt, string_constraintst >	add_axioms_for_index_of (const function_application_exprt &f)
	Index of the first occurence of a target inside the string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_last_index_of_string (const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
	Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. More...
std::pair< exprt, string_constraintst >	add_axioms_for_last_index_of (const array_string_exprt &str, const exprt &c, const exprt &from_index)
	Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. More...
std::pair< exprt, string_constraintst >	add_axioms_for_last_index_of (const function_application_exprt &f)
	Index of the last occurence of a target inside the string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_string_of_float (const function_application_exprt &f)
	String representation of a float value. More...
std::pair< exprt, string_constraintst >	add_axioms_for_string_of_float (const array_string_exprt &res, const exprt &f)
	Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More...
std::pair< exprt, string_constraintst >	add_axioms_for_fractional_part (const array_string_exprt &res, const exprt &int_expr, size_t max_size)
	Add axioms for representing the fractional part of a floating point starting with a dot. More...
std::pair< exprt, string_constraintst >	add_axioms_from_float_scientific_notation (const array_string_exprt &res, const exprt &f)
	Add axioms to write the float in scientific notation. More...
std::pair< exprt, string_constraintst >	add_axioms_from_float_scientific_notation (const function_application_exprt &f)
	Representation of a float value in scientific notation. More...
std::pair< exprt, string_constraintst >	add_axioms_from_double (const function_application_exprt &f)
	Add axioms corresponding to the String.valueOf(D) java function. More...
std::pair< exprt, string_constraintst >	add_axioms_for_replace (const function_application_exprt &f)
	Replace a character by another in a string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_set_length (const function_application_exprt &f)
	Reduce or extend a string to have the given length. More...
std::pair< exprt, string_constraintst >	add_axioms_for_substring (const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
	Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. More...
std::pair< exprt, string_constraintst >	add_axioms_for_substring (const function_application_exprt &f)
	Substring of a string between two indices. More...
std::pair< exprt, string_constraintst >	add_axioms_for_trim (const function_application_exprt &f)
	Remove leading and trailing whitespaces. More...
std::pair< exprt, string_constraintst >	add_axioms_for_code_point (const array_string_exprt &res, const exprt &code_point)
	add axioms for the conversion of an integer representing a java code point to a utf-16 string More...
std::pair< exprt, string_constraintst >	add_axioms_for_char_literal (const function_application_exprt &f)
	add axioms stating that the returned value is equal to the argument More...
std::pair< exprt, string_constraintst >	add_axioms_for_code_point_count (const function_application_exprt &f)
	Add axioms corresponding the String.codePointCount java function. More...
std::pair< exprt, string_constraintst >	add_axioms_for_offset_by_code_point (const function_application_exprt &f)
	Add axioms corresponding the String.offsetByCodePointCount java function. More...
string_constraintst	add_axioms_for_characters_in_integer_string (const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
	Add axioms connecting the characters in the input string to the value of the output integer. More...
std::vector< exprt >	get_conjuncts_for_correct_number_format (const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
	Add axioms making the return value true if the given string is a correct number in the given radix. More...
std::pair< exprt, string_constraintst >	add_axioms_for_parse_int (const function_application_exprt &f)
	Integer value represented by a string. More...
std::pair< exprt, string_constraintst >	add_axioms_for_is_valid_int (const function_application_exprt &f)
	Check a string is a valid integer, using the same rules as Java Integer.parseInt. More...
std::pair< exprt, string_constraintst >	add_axioms_for_compare_to (const function_application_exprt &f)
	Lexicographic comparison of two strings. More...
std::pair< exprt, string_constraintst >	combine_results (std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
	Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints. More...
parseint_argumentst	unpack_parseint_arguments (const function_application_exprt &f, const typet &target_int_type)

Public Attributes
symbol_generatort	fresh_symbol
array_poolt	array_pool
const namespacet	ns

Private Member Functions
exprt	associate_array_to_pointer (const exprt &return_code, const function_application_exprt &f)
	Associate a char array to a char pointer. More...
exprt	associate_length_to_array (const exprt &return_code, const function_application_exprt &f)
	Associate an integer length to a char array. More...

Private Attributes
message_handlert &	message_handler

Detailed Description

Definition at line 47 of file string_constraint_generator.h.

Constructor & Destructor Documentation

string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort	(	const namespacet &	ns,
		message_handlert &	message_handler
	)

Definition at line 33 of file string_constraint_generator_main.cpp.

Member Function Documentation

add_axioms_for_char_at()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_char_at

(

const function_application_exprt &

f

)

Character at a given position.

Add axioms stating that the character of the string at position given by second argument is equal to the returned value. This axiom is \( char = str[i] \).

Parameters

f	function application with arguments string str and integer i

Returns

character expression char

Definition at line 387 of file string_constraint_generator_main.cpp.

add_axioms_for_char_literal()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_char_literal

(

const function_application_exprt &

f

)

add axioms stating that the returned value is equal to the argument

Parameters

f	function application with one character argument

Returns

a new character expression

Definition at line 350 of file string_constraint_generator_main.cpp.

add_axioms_for_characters_in_integer_string()

string_constraintst string_constraint_generatort::add_axioms_for_characters_in_integer_string	(	const exprt &	input_int,
		const typet &	type,
		const bool	strict_formatting,
		const array_string_exprt &	str,
		const std::size_t	max_string_length,
		const exprt &	radix,
		const unsigned long	radix_ul
	)

Add axioms connecting the characters in the input string to the value of the output integer.

It is constructive because it gives a formula for input_int in terms of the characters in str.

Parameters

input_int	the integer represented by str
type	the type for input_int
strict_formatting	if true, don't allow a leading plus, redundant zeros or upper case letters
str	input string
max_string_length	the maximum length str can have
radix	the radix, with the same type as input_int
radix_ul	the radix as an unsigned long, or 0 if that can't be determined

Deal with size==1 case separately. There are axioms from add_axioms_for_correct_number_format which say that the string must contain at least one digit, so we don't have to worry about "+" or "-".

Definition at line 373 of file string_constraint_generator_valueof.cpp.

add_axioms_for_code_point()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_code_point	(	const array_string_exprt &	res,
		const exprt &	code_point
	)

add axioms for the conversion of an integer representing a java code point to a utf-16 string

Parameters

res	array of characters corresponding to the result fo the function
code_point	an expression representing a java code point

Returns

integer expression equal to zero

Definition at line 23 of file string_constraint_generator_code_points.cpp.

add_axioms_for_code_point_at()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_code_point_at

(

const function_application_exprt &

f

)

add axioms corresponding to the String.codePointAt java function

Parameters

f	function application with arguments a string and an index

Returns

a integer expression corresponding to a code point

Definition at line 124 of file string_constraint_generator_code_points.cpp.

add_axioms_for_code_point_before()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_code_point_before

(

const function_application_exprt &

f

)

add axioms corresponding to the String.codePointBefore java function

parameters: function application with two arguments: a string and an

index

Returns

a integer expression corresponding to a code point

Definition at line 156 of file string_constraint_generator_code_points.cpp.

add_axioms_for_code_point_count()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_code_point_count

(

const function_application_exprt &

f

)

Add axioms corresponding the String.codePointCount java function.

add axioms giving approximate bounds on the result of the String.codePointCount java function

Deprecated:

This is Java specific and should be implemented in Java.

"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, should be implemented in Java"

Parameters

f	function application with three arguments string str, integer begin and integer end.

Returns

an integer expression

Definition at line 191 of file string_constraint_generator_code_points.cpp.

add_axioms_for_compare_to()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_compare_to

(

const function_application_exprt &

f

)

Lexicographic comparison of two strings.

Add axioms ensuring the result corresponds to that of the String.compareTo Java function. In the lexicographic comparison, x representing the first point where the two strings differ, we add axioms:

• \( res=0 \Rightarrow |s1|=|s2|\)
• \( \forall i<|s1|. s1[i]=s2[i] \)
• \( \exists x.\ res\ne 0 \Rightarrow x > 0 \land ((|s1| \ge |s2| \land x<|s1|) \lor (|s1| \ge |s2| \land x<|s2|) \land res=s1[x]-s2[x] ) \lor cond2: (|s1|<|s2| \land x=|s1|) \lor (|s1| > |s2| \land x=|s2|) \land res=|s1|-|s2|) \)
• \( \forall i'<x. res\ne 0 \Rightarrow s1[i]=s2[i] \)

  Parameters

  f	function application with arguments refined_string s1 and refined_string s2

  Returns

  integer expression res

Definition at line 209 of file string_constraint_generator_comparison.cpp.

add_axioms_for_concat()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_concat	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2
	)

Add axioms enforcing that res is equal to the concatenation of s1 and s2.

Deprecated:

should use concat_substr instead

Parameters

res	string_expression corresponding to the result
s1	the string expression to append to
s2	the string expression to append to the first one

Returns

an integer expression

Definition at line 160 of file string_concatenation_builtin_function.cpp.

add_axioms_for_concat_code_point()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_concat_code_point

(

const function_application_exprt &

f

)

Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.

Deprecated:

java specific

Parameters

f	function application with two arguments: a string and a code point

Returns

an expression

Definition at line 175 of file string_concatenation_builtin_function.cpp.

add_axioms_for_concat_substr()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_concat_substr	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		const exprt &	start_index,
		const exprt &	end_index
	)

Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at indexend_index'‘.

Where start_index’ is max(0, start_index) and end_index' is max(min(end_index, s2.length), start_index') If s1.length + end_index' - start_index' is greater than the maximal integer of the type of res.length, then the result gets truncated to the size of this maximal integer.

These axioms are:

1. \(|res| = overflow ? |s_1| + end\_index' - start\_index' : max_int \)
2. \(\forall i<|s_1|. res[i]=s_1[i] \)
3. \(\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\)

Parameters

res	an array of characters expression
s1	an array of characters expression
s2	an array of characters expression
start_index	integer expression
end_index	integer expression

Returns

integer expression 0

Definition at line 53 of file string_concatenation_builtin_function.cpp.

add_axioms_for_constant()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_constant	(	const array_string_exprt &	res,
		irep_idt	sval,
		const exprt &	guard = true_exprt()
	)

Add axioms ensuring that the provided string expression and constant are equal.

Parameters

res	array of characters for the result
sval	a string constant
guard	condition under which the axiom should apply, true by default

Returns

integer expression equal to zero

Definition at line 24 of file string_constraint_generator_constants.cpp.

add_axioms_for_constrain_characters()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_constrain_characters

(

const function_application_exprt &

f

)

Add axioms to ensure all characters of a string belong to a given set.

The axiom is: \(\forall i \in [start, end).\ s[i] \in char_set \), where char_set is given by the string char_set_string composed of three characters low_char, - and high_char. Character c belongs to char_set if \(low_char \le c \le high_char\).

Parameters

f	a function application with arguments: integer |s|, character pointer &s[0], string char_set_string, optional integers start and end

Returns

integer expression whose value is zero

Definition at line 163 of file string_constraint_generator_main.cpp.

add_axioms_for_contains()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_contains

(

const function_application_exprt &

f

)

Test whether a string contains another.

Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:

1. \( contains \Rightarrow |s_0| \ge |s_1| \)
2. \( contains \Rightarrow 0 \le startpos \le |s_0|-|s_1| \)
3. \( !contains \Rightarrow startpos = -1 \)
4. \( \forall qvar < |s_1|.\ contains \Rightarrow s_1[qvar] = s_0[startpos + qvar] \)
5. \( \forall startpos \le |s_0|-|s_1|. \ (!contains \land |s_0| \ge |s_1|) \Rightarrow \exists witness < |s_1|. \ s_1[witness] \ne s_0[startpos+witness] \)

   Warning

   slow for target longer than one character

   Parameters

   f	function application with arguments refined_string s0 refined_string s1

   Returns

   Boolean expression contains

Definition at line 250 of file string_constraint_generator_testing.cpp.

add_axioms_for_copy()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_copy

(

const function_application_exprt &

f

)

add axioms to say that the returned string expression is equal to the argument of the function application

Deprecated:

should use substring instead

Parameters

f	function application with one argument, which is a string, or three arguments: string, integer offset and count

Returns

a new string expression

Deprecated:

"deprecated since " "2017" "-" "10" "-" "5" "; " "should use substring instead"

Definition at line 311 of file string_constraint_generator_main.cpp.

add_axioms_for_cprover_string()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_cprover_string	(	const array_string_exprt &	res,
		const exprt &	arg,
		const exprt &	guard
	)

Convert an expression of type string_typet to a string_exprt.

Parameters

res	string expression for the result
arg	expression of type string typet
guard	condition under which res should be equal to arg

Returns

0 if constraints were added, 1 if expression could not be handled and no constraint was added. Expression we can handle are of the form \( e := "<string constant>" | (expr)? e : e \)

Definition at line 83 of file string_constraint_generator_constants.cpp.

add_axioms_for_delete() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_delete	(	const array_string_exprt &	res,
		const array_string_exprt &	str,
		const exprt &	start,
		const exprt &	end
	)

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included).

These axioms are the same as would be generated for: concat(substring(str, 0, start), substring(end, |str|)) (see add_axioms_for_substring and add_axioms_for_concat_substr).

Parameters

res	array of characters expression
str	array of characters expression
start	integer expression
end	integer expression

Returns

integer expression different from zero to signal an exception

Definition at line 383 of file string_constraint_generator_transformation.cpp.

add_axioms_for_delete() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_delete

(

const function_application_exprt &

f

)

Remove a portion of a string.

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). (More...)

Parameters

f	function application with arguments integer |res|, character pointer &res[0], refined_string str, integer start and integer end

Returns

an integer expression whose value is different from 0 to signal an exception

Definition at line 418 of file string_constraint_generator_transformation.cpp.

add_axioms_for_delete_char_at()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_delete_char_at

(

const function_application_exprt &

f

)

add axioms corresponding to the StringBuilder.deleteCharAt java function

Parameters

f	function application with two arguments, the first is a string and the second is an index

Returns

an expression whose value is non null to signal an exception

Definition at line 356 of file string_constraint_generator_transformation.cpp.

add_axioms_for_empty_string()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_empty_string

(

const function_application_exprt &

f

)

Add axioms to say that the returned string expression is empty.

Parameters

f	function application with arguments integer length and character pointer ptr.

Returns

integer expression equal to zero

Definition at line 64 of file string_constraint_generator_constants.cpp.

add_axioms_for_equals()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_equals

(

const function_application_exprt &

f

)

Equality of the content of two strings.

Add axioms stating that the result is true exactly when the strings represented by the arguments are equal. These axioms are:

1. \( eq \Rightarrow |s_1|=|s_2|\)
2. \( \forall i<|s_1|.\ eq \Rightarrow s_1[i]=s_2[i] \)
3. \( \lnot eq \Rightarrow (|s_1| \ne |s_2| \land witness=-1) \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \)

   Parameters

   f	function application with arguments refined_string s1 and refined_string s2

   Returns

   Boolean expression eq

Definition at line 31 of file string_constraint_generator_comparison.cpp.

add_axioms_for_equals_ignore_case()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_equals_ignore_case

(

const function_application_exprt &

f

)

Equality of the content ignoring case of characters.

Add axioms ensuring the result is true when the two strings are equal if case is ignored. These axioms are:

1. \( eq \Rightarrow |s_1|=|s_2|\)
2. \( \forall i \in [0, |s_1|). \ eq \Rightarrow {\tt equal\_ignore\_case}(s_1[i],s_2[i]) \)
3. \( \lnot eq \Rightarrow |s_1| \ne |s_2| \lor (0 \le witness<|s_1| \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \)

   Parameters

   f	function application with arguments refined_string s1 and refined_string s2

   Returns

   Boolean expression eq

Definition at line 136 of file string_constraint_generator_comparison.cpp.

add_axioms_for_fractional_part()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_fractional_part	(	const array_string_exprt &	res,
		const exprt &	int_expr,
		size_t	max_size
	)

Add axioms for representing the fractional part of a floating point starting with a dot.

Parameters

res	string expression for the result
int_expr	an integer expression
max_size	a maximal size for the string, this includes the potential minus sign and therefore should be greater than 2

Returns

code 0 on success

Definition at line 244 of file string_constraint_generator_float.cpp.

add_axioms_for_function_application()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_function_application

(

const function_application_exprt &

expr

)

strings contained in this call are converted to objects of type string_exprt, through adding axioms.

Axioms are then added to enforce that the result corresponds to the function application.

Parameters

expr	an expression containing a function application

Returns

expression corresponding to the result of the function application

Definition at line 214 of file string_constraint_generator_main.cpp.

add_axioms_for_index_of() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_index_of	(	const array_string_exprt &	str,
		const exprt &	c,
		const exprt &	from_index
	)

Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index.

These axioms are:

1. \(-1 \le {\tt index} < |{\tt haystack}| \)
2. \( \lnot contains \Leftrightarrow {\tt index} = -1 \)
3. \( contains \Rightarrow {\tt from\_index} \le {\tt index} \land {\tt haystack}[{\tt index}] = {\tt needle} \)
4. \( \forall i \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow {\tt haystack}[i] \ne {\tt needle} \)
5. \( \forall m, n \in [{\tt from\_index}, |{\tt haystack}|) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle} \)

   Parameters

   str	an array of characters expression
   c	a character expression
   from_index	an integer expression

   Returns

   integer expression index

Definition at line 41 of file string_constraint_generator_indexof.cpp.

add_axioms_for_index_of() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_index_of

(

const function_application_exprt &

f

)

Index of the first occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. (More...)

Warning

slow for string targets

Parameters

f	function application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value 0

Returns

integer expression

Definition at line 309 of file string_constraint_generator_indexof.cpp.

add_axioms_for_index_of_string()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_index_of_string	(	const array_string_exprt &	haystack,
		const array_string_exprt &	needle,
		const exprt &	from_index
	)

Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index.

If needle is an empty string then the result is from_index.

These axioms are:

1. \( contains \Rightarrow {\tt from\_index} \le \tt{index} \le |{\tt haystack}|-|{\tt needle} | \)
2. \( \lnot contains \Leftrightarrow {\tt index} = -1 \)
3. \( \forall n \in [0,|{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n + {\tt index}] = {\tt needle}[n] \)
4. \( \forall n \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|).\ {\tt haystack}[m+n] \ne {\tt needle}[m]]) \)
5. \( \forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \)
6. \( |{\tt needle}| = 0 \Rightarrow \tt{index} = from_index \)

   Parameters

   haystack	an array of character expression
   needle	an array of character expression
   from_index	an integer expression

   Returns

   integer expression index representing the first index of needle in haystack

Definition at line 115 of file string_constraint_generator_indexof.cpp.

add_axioms_for_insert()

std::pair<exprt, string_constraintst> string_constraint_generatort::add_axioms_for_insert	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		const exprt &	offset
	)

add_axioms_for_is_empty()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_empty

(

const function_application_exprt &

f

)

Add axioms stating that the returned value is true exactly when the argument string is empty.

Deprecated:

should use string_length(s)==0 instead

Parameters

f	function application with a string argument

Returns

a Boolean expression

Deprecated:

"deprecated since " "2017" "-" "10" "-" "5" "; " "should use `string_length s == 0` instead"

Definition at line 130 of file string_constraint_generator_testing.cpp.

add_axioms_for_is_prefix() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_prefix	(	const array_string_exprt &	prefix,
		const array_string_exprt &	str,
		const exprt &	offset
	)

Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset.

These axioms are:

1. isprefix => offset_within_bounds
2. forall qvar in [0, |prefix|). isprefix => str[qvar + offset] = prefix[qvar]
3. !isprefix => !offset_within_bounds || 0 <= witness < |prefix| && str[witness+offset] != prefix[witness]

where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|

Parameters

prefix	an array of characters
str	an array of characters
offset	an integer

Returns

Boolean expression isprefix

Definition at line 38 of file string_constraint_generator_testing.cpp.

add_axioms_for_is_prefix() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_prefix	(	const function_application_exprt &	f,
		bool	swap_arguments
	)

Test if the target is a prefix of the string.

Add axioms ensuring the return value is true when the string starts with the given target. These axioms are detailed here: string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)

Parameters

f	a function application with arguments refined_string s0, refined string s1 and optional integer argument offsetwhose default value is 0
swap_arguments	a Boolean telling whether the prefix is the second argument or the first argument

Returns

boolean expression isprefix

Definition at line 106 of file string_constraint_generator_testing.cpp.

add_axioms_for_is_suffix()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_suffix	(	const function_application_exprt &	f,
		bool	swap_arguments
	)

Test if the target is a suffix of the string.

Add axioms ensuring the return value is true when the first string ends with the given target. These axioms are:

1. \( \texttt{issuffix} \Rightarrow |s_0| \ge |s_1| \)
2. \( \forall i <|s_1|.\ {\tt issuffix} \Rightarrow s_1[i] = s_0[i + |s_0| - |s_1|] \)
3. \( \lnot {\tt issuffix} \Rightarrow (|s_1| > |s_0| \land {\tt witness}=-1) \lor (|s_1| > {witness} \ge 0 \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \)

Parameters

f	a function application with arguments refined_string s0 and refined_string s1
swap_arguments	boolean flag telling whether the suffix is the second argument or the first argument

Returns

Boolean expression issuffix

Deprecated:

Should use strings_startwith(s0, s1, s1.length - s0.length).

"deprecated since " "2018" "-" "6" "-" "6" "; " "should use strings_startwith"

Definition at line 171 of file string_constraint_generator_testing.cpp.

add_axioms_for_is_valid_int()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_valid_int

(

const function_application_exprt &

f

)

Check a string is a valid integer, using the same rules as Java Integer.parseInt.

Add axioms relating a boolean return value to being a valid integer

Parameters

f	a function application with arguments refined_string str and an optional integer for the radix

Returns

boolean expression indicating whether the string is a valid integer

Note

the only thing stopping us from taking longer strings with many leading zeros is the axioms for correct number format

Definition at line 489 of file string_constraint_generator_valueof.cpp.

add_axioms_for_last_index_of() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_last_index_of	(	const array_string_exprt &	str,
		const exprt &	c,
		const exprt &	from_index
	)

Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index.

These axioms are :

1. \( -1 \le {\tt index} \le {\tt from\_index} \land {\tt index} < |{\tt haystack}| \)
2. \( {\tt index} = -1 \Leftrightarrow \lnot contains\)
3. \( contains \Rightarrow {\tt haystack}[{\tt index}] = {\tt needle} )\)
4. \( \forall n \in [{\tt index} +1, min({\tt from\_index}+1, |{\tt haystack}|)) .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle} \)
5. \( \forall m \in [0, min({\tt from\_index}+1, |{\tt haystack}|)) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\)

   Parameters

   str	an array of characters expression
   c	a character expression
   from_index	an integer expression

   Returns

   integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 363 of file string_constraint_generator_indexof.cpp.

add_axioms_for_last_index_of() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_last_index_of

(

const function_application_exprt &

f

)

Index of the last occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. (More...)

Warning

slow for string targets

Parameters

f	function application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value |haystack|-1

Returns

an integer expression

Definition at line 433 of file string_constraint_generator_indexof.cpp.

add_axioms_for_last_index_of_string()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_last_index_of_string	(	const array_string_exprt &	haystack,
		const array_string_exprt &	needle,
		const exprt &	from_index
	)

Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index.

If needle is the empty string, the result is from_index.

These axioms are:

1. \( contains \Rightarrow -1 \le {\tt index} \land {\tt index} \le {\tt from\_index} \land {\tt index} \le |{\tt haystack}| - |{\tt needle}| \)
2. \( \lnot contains \Leftrightarrow {\tt index}= -1 \)
3. \( \forall n \in [0, |{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n+{\tt index}] = {\tt needle}[n] \)
4. \( \forall n \in [{\tt index}+1, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]]) \)
5. \( \forall n \in [0, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \)
6. \( |{\tt needle}| = 0 \Rightarrow index = from_index \)

   Parameters

   haystack	an array of characters expression
   needle	an array of characters expression
   from_index	integer expression

   Returns

   integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 216 of file string_constraint_generator_indexof.cpp.

add_axioms_for_length()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_length

(

const function_application_exprt &

f

)

Length of a string.

Returns the length of the string argument of the given function application

Parameters

f	function application with argument string str

Returns

expression |str|

Definition at line 331 of file string_constraint_generator_main.cpp.

add_axioms_for_offset_by_code_point()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_offset_by_code_point

(

const function_application_exprt &

f

)

Add axioms corresponding the String.offsetByCodePointCount java function.

add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.

Deprecated:

This is Java specific and should be implemented in Java.

"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, should be implemented in Java"

We approximate the result by saying the result is between index + offset and index + 2 * offset

Parameters

f	function application with arguments string str, integer index and integer offset.

Returns

a new string expression

Definition at line 217 of file string_constraint_generator_code_points.cpp.

add_axioms_for_parse_int()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_parse_int

(

const function_application_exprt &

f

)

Integer value represented by a string.

Add axioms ensuring the value of the returned integer corresponds to the value represented by str

Parameters

f	a function application with arguments refined_string str and an optional integer for the radix

Returns

integer expression equal to the value represented by str

Definition at line 525 of file string_constraint_generator_valueof.cpp.

add_axioms_for_replace()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_replace

(

const function_application_exprt &

f

)

Replace a character by another in a string.

Add axioms ensuring that res corresponds to str where occurences of old_char have been replaced by new_char. These axioms are:

1. \( |{\tt res}| = |{\tt str}| \)
2. \( \forall i \in 0, |{\tt res}|) .\ {\tt str}[i]={\tt old\_char} \Rightarrow {\tt res}[i]={\tt new\_char} \land {\tt str}[i]\ne {\tt old\_char} \Rightarrow {\tt res}[i]={\tt str}[i] \) Only supports String.replace(char, char) and String.replace(String, String) for single-character strings Returns original string in every other case (that behaviour is to be fixed in the future)

   Parameters

   f	function application with arguments integer |res|, character pointer &res[0], refined_string str, character old_char and character new_char

   Returns

   an integer expression equal to 0

Definition at line 313 of file string_constraint_generator_transformation.cpp.

add_axioms_for_set_length()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_set_length

(

const function_application_exprt &

f

)

Reduce or extend a string to have the given length.

Add axioms ensuring the returned string expression res has length max(k, 0) and characters at position i in res are equal to the character at position i in s1 if i is smaller that the length of s1, otherwise it is the null character \u0000. Note this means if k is negative then the string is truncated to length 0; in practice a wrapper function will usually handle this case.

These axioms are:

1. \( |{\tt res}|={\tt k} \)
2. \( \forall i<|{\tt res}|.\ i < |s_1| \Rightarrow {\tt res}[i] = s_1[i] \)
3. \( \forall i<|{\tt res}|.\ i \ge |s_1| \Rightarrow {\tt res}[i] = 0 \)

   Parameters

   f	function application with arguments integer |res|, character pointer &res[0], refined_string s1, integer k

   Returns

   integer expression equal to 0

Definition at line 39 of file string_constraint_generator_transformation.cpp.

add_axioms_for_string_of_float() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_string_of_float	(	const array_string_exprt &	res,
		const exprt &	f
	)

Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '.

', followed by one or more decimal digits representing the fractional part of m. This specification is correct for inputs that do not exceed 100000 and the function is unspecified for other values.

Parameters

res	string expression corresponding to the result
f	a float expression, which is positive

Returns

an integer expression, different from zero if an error should be raised

Definition at line 192 of file string_constraint_generator_float.cpp.

add_axioms_for_string_of_float() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_string_of_float

(

const function_application_exprt &

f

)

String representation of a float value.

We currently only specify that the string for NaN is "NaN", for infinity and minus infinity the string are "Infinity" and "-Infinity respectively otherwise the string contains only characters in [0123456789.] and '-' at the start for negative number

Add axioms corresponding to the String.valueOf(F) java function

Parameters

f	function application with one float argument

Returns

an integer expression

Definition at line 161 of file string_constraint_generator_float.cpp.

add_axioms_for_string_of_int()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_string_of_int	(	const array_string_exprt &	res,
		const exprt &	input_int,
		size_t	max_size
	)

Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression.

Parameters

res	string expression for the result
input_int	a signed integer expression
max_size	a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")

Returns

code 0 on success

Definition at line 117 of file string_constraint_generator_valueof.cpp.

add_axioms_for_string_of_int_with_radix()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_string_of_int_with_radix	(	const array_string_exprt &	res,
		const exprt &	input_int,
		const exprt &	radix,
		size_t	max_size
	)

Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression.

Parameters

res	string expression for the result
input_int	a signed integer expression
radix	the radix to use
max_size	a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")

Returns

code 0 on success

Most of the time we can evaluate radix as an integer. The value 0 is used to indicate when we can't tell what the radix is.

Definition at line 137 of file string_constraint_generator_valueof.cpp.

add_axioms_for_substring() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_substring	(	const array_string_exprt &	res,
		const array_string_exprt &	str,
		const exprt &	start,
		const exprt &	end
	)

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`.

An actual java program should throw an exception in that case.

These axioms are:

1. \( |{\tt res}| = end' - start' \)
2. \( \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \)

   Parameters

   res	array of characters expression
   str	array of characters expression
   start	integer expression
   end	integer expression

   Returns

   integer expression equal to zero

Definition at line 124 of file string_constraint_generator_transformation.cpp.

add_axioms_for_substring() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_substring

(

const function_application_exprt &

f

)

Substring of a string between two indices.

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. (More...)

Warning

The specification may not be correct for the case where the string is shorter than the end index

Parameters

f	function application with arguments integer |res|, character pointer &res[0], refined_string str, integer start, optional integer end with default value |str|.

Returns

integer expression which is different from 0 when there is an exception to signal

Definition at line 96 of file string_constraint_generator_transformation.cpp.

add_axioms_for_trim()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_trim

(

const function_application_exprt &

f

)

Remove leading and trailing whitespaces.

Add axioms ensuring res corresponds to str from which leading and trailing whitespaces have been removed. Are considered whitespaces, characters whose ascii code are smaller than that of ' ' (space).

These axioms are:

1. \( idx + |{\tt res}| \le |{\tt str}| \) where idx represents the index of the first non-space character.
2. \( idx \ge 0 \)
3. \( |{\tt str}| \ge idx \)
4. \( |{\tt res}| \ge 0 \)
5. \( |{\tt res}| \le |{\tt str}| \) (this is necessary to prevent exceeding the biggest integer)
6. \( \forall n<m.\ {\tt str}[n] \le \lq~\rq \)
7. \( \forall n<|{\tt str}|-m-|{\tt res}|.\ {\tt str}[m+|{\tt res}|+n] \le \lq~\rq \)
8. \( \forall n<|{\tt res}|.\ {\tt str}[idx+n]={\tt res}[n] \)
9. \( (s[m]>{\tt \lq~\rq} \land s[m+|{\tt res}|-1]>{\tt \lq~\rq}) \lor m=|{\tt res}| \)

   Note

   Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant

   Parameters

   f	function application with arguments integer |res|, character pointer &res[0], refined_string str.

   Returns

   integer expression which is different from 0 when there is an exception to signal

Definition at line 183 of file string_constraint_generator_transformation.cpp.

add_axioms_from_bool() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_bool	(	const array_string_exprt &	res,
		const exprt &	b
	)

Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false.

Deprecated:

This is Java specific and should be implemented in Java instead

Parameters

res	string expression for the result
b	Boolean expression

Returns

code 0 on success

Deprecated:

"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, should be implemented in Java"

Definition at line 65 of file string_constraint_generator_valueof.cpp.

add_axioms_from_bool() [2/2]

std::pair<exprt, string_constraintst> string_constraint_generatort::add_axioms_from_bool

(

const function_application_exprt &

f

)

add_axioms_from_char() [1/2]

std::pair<exprt, string_constraintst> string_constraint_generatort::add_axioms_from_char	(	const array_string_exprt &	res,
		const exprt &	c
	)

add_axioms_from_char() [2/2]

std::pair<exprt, string_constraintst> string_constraint_generatort::add_axioms_from_char

(

const function_application_exprt &

f

)

add_axioms_from_double()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_double

(

const function_application_exprt &

f

)

Add axioms corresponding to the String.valueOf(D) java function.

Parameters

f	function application with one double argument

Returns

an integer expression

Definition at line 173 of file string_constraint_generator_float.cpp.

add_axioms_from_float_scientific_notation() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_float_scientific_notation	(	const array_string_exprt &	res,
		const exprt &	float_expr
	)

Add axioms to write the float in scientific notation.

A float is represented as \(f = m * 2^e\) where \(0 <= m < 2\) is the significand and \(-126 <= e <= 127\) is the exponent. We want an alternate representation by finding \(n\) and \(d\) such that \(f=n*10^d\). We can estimate \(d\) the following way: \(d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\) \(d = floor(log_10(2) * e)\) Then \(n\) can be expressed by the equation: \(log_10(n) = log_10(m) + log_10(2) * e - d\) \(n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\)

Parameters

res	string expression representing the float in scientific notation
float_expr	a float expression, which is positive

Returns

a integer expression different from 0 to signal an exception

Definition at line 337 of file string_constraint_generator_float.cpp.

add_axioms_from_float_scientific_notation() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_float_scientific_notation

(

const function_application_exprt &

f

)

Representation of a float value in scientific notation.

Add axioms corresponding to the scientific representation of floating point values

Parameters

f	a function application expression

Returns

code 0 on success

Definition at line 527 of file string_constraint_generator_float.cpp.

add_axioms_from_int_hex() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_int_hex	(	const array_string_exprt &	res,
		const exprt &	i
	)

Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.

Deprecated:

use add_axioms_from_int_with_radix instead

Parameters

res	string expression for the result
i	an integer argument

Returns

code 0 on success

Deprecated:

"deprecated since " "2017" "-" "10" "-" "5" "; " "use add_axioms_for_string_of_int_with_radix"

Definition at line 200 of file string_constraint_generator_valueof.cpp.

add_axioms_from_int_hex() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_int_hex

(

const function_application_exprt &

f

)

Add axioms corresponding to the Integer.toHexString(I) java function.

Parameters

f	function application with an integer argument

Returns

code 0 on success

Definition at line 259 of file string_constraint_generator_valueof.cpp.

add_axioms_from_literal()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_literal

(

const function_application_exprt &

f

)

String corresponding to an internal cprover string.

Add axioms ensuring that the returned string expression is equal to the string literal.

Parameters

f	function application with an argument which is a string literal that is a constant with a string value.

Returns

string expression

Definition at line 111 of file string_constraint_generator_constants.cpp.

add_axioms_from_long()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_long

(

const function_application_exprt &

f

)

Add axioms corresponding to the String.valueOf(J) java function.

Deprecated:

should use add_axioms_from_int instead

Parameters

f	function application with one long argument

Returns

a new string expression

Deprecated:

"deprecated since " "2017" "-" "10" "-" "5" "; " "use add_axioms_for_string_of_int instead"

Definition at line 44 of file string_constraint_generator_valueof.cpp.

add_constraint_on_characters()

string_constraintst string_constraint_generatort::add_constraint_on_characters	(	const array_string_exprt &	s,
		const exprt &	start,
		const exprt &	end,
		const std::string &	char_set
	)

Add constraint on characters of a string.

This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)

Parameters

s	a string expression
start	index of the first character to constrain
end	index at which we stop adding constraints
char_set	a string of the form "<low_char>-<high_char>" where <low_char> and <high_char> are two characters, which represents the set of characters that are between low_char and high_char.

Returns

a string expression that is linked to the argument through axioms that are added to the list

Definition at line 129 of file string_constraint_generator_main.cpp.

associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const exprt &  return_code, const function_application_exprt &  f  )

private

Associate a char array to a char pointer.

Insert in array_pool a binding from ptr to arr. If the length of arr is infinite, a new integer symbol is created and stored in array_pool. This also adds the default axioms for arr.

Parameters

return_code	expression which is assigned the result of the function
f	a function application with argument a character array arr and a character pointer ptr.

Returns

a constraint

Definition at line 63 of file string_constraint_generator_main.cpp.

associate_length_to_array()

exprt string_constraint_generatort::associate_length_to_array ( const exprt &  return_code, const function_application_exprt &  f  )

private

Associate an integer length to a char array.

This adds an axiom ensuring that arr.length and length are equal.

Parameters

return_code	expression which is assigned the result of the function
f	a function application with argument a character array arr and an integer length.

Returns

a constraint

Definition at line 87 of file string_constraint_generator_main.cpp.

combine_results()

std::pair< exprt, string_constraintst > string_constraint_generatort::combine_results	(	std::pair< exprt, string_constraintst >	result1,
		std::pair< exprt, string_constraintst >	result2
	)

Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints.

Definition at line 420 of file string_constraint_generator_main.cpp.

get_conjuncts_for_correct_number_format()

std::vector< exprt > string_constraint_generatort::get_conjuncts_for_correct_number_format	(	const array_string_exprt &	str,
		const exprt &	radix_as_char,
		const unsigned long	radix_ul,
		const std::size_t	max_size,
		const bool	strict_formatting
	)

Add axioms making the return value true if the given string is a correct number in the given radix.

Parameters

str	string expression
radix_as_char	the radix as an expression of the same type as the characters in str
radix_ul	the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
max_size	maximum number of characters
strict_formatting	if true, don't allow a leading plus, redundant zeros or upper case letters

index < length => is_digit_with_radix(str[index], radix)

Definition at line 279 of file string_constraint_generator_valueof.cpp.

make_array_pointer_association()

std::optional< exprt > string_constraint_generatort::make_array_pointer_association	(	const exprt &	return_code,
		const function_application_exprt &	expr
	)

Associate array to pointer, and array to length.

Returns

an expression if the given function application is one of associate pointer and associate length

Definition at line 196 of file string_constraint_generator_main.cpp.

unpack_parseint_arguments()

string_constraint_generatort::parseint_argumentst string_constraint_generatort::unpack_parseint_arguments	(	const function_application_exprt &	f,
		const typet &	target_int_type
	)

Definition at line 458 of file string_constraint_generator_valueof.cpp.

Member Data Documentation

array_pool

array_poolt string_constraint_generatort::array_pool

Definition at line 63 of file string_constraint_generator.h.

fresh_symbol

symbol_generatort string_constraint_generatort::fresh_symbol

Definition at line 61 of file string_constraint_generator.h.

message_handler

message_handlert& string_constraint_generatort::message_handler

private

Definition at line 75 of file string_constraint_generator.h.

ns

const namespacet string_constraint_generatort::ns

Definition at line 65 of file string_constraint_generator.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator.h
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_concatenation_builtin_function.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_code_points.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_comparison.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_constants.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_float.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_indexof.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_main.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_testing.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_transformation.cpp
• /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_valueof.cpp