cprover
string_constraint_generator_valueof.cpp File Reference

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...

Include dependency graph for string_constraint_generator_valueof.cpp:

Go to the source code of this file.

Functions

 DEPRECATED ("use add_axioms_for_string_of_int which takes a radix argument instead") exprt string_constraint_generatort
 Add axioms stating that the string res corresponds to the integer argument written in hexadecimal. More...
 
exprt is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
 Check if a character is a digit with respect to the given radix, e.g. More...
 
exprt get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
 Get the numeric value of a character, assuming that the radix is large enough. More...
 
size_t max_printed_string_length (const typet &type, unsigned long radix_ul)
 Calculate the string length needed to represent any value of the given type using the given radix. More...
 

Detailed Description

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.

Definition in file string_constraint_generator_valueof.cpp.

Function Documentation

◆ DEPRECATED()

DEPRECATED ( "use add_axioms_for_string_of_int which takes a radix argument instead"  )

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

Deprecated:
use add_axioms_from_int which takes a radix argument instead
Parameters
resstring expression for the result
ian integer argument
Returns
code 0 on success

Definition at line 208 of file string_constraint_generator_valueof.cpp.

References char_type(), from_integer(), irept::id(), index_type(), is_number(), PRECONDITION, and typet::subtype().

◆ get_numeric_value_from_character()

exprt get_numeric_value_from_character ( const exprt chr,
const typet char_type,
const typet type,
const bool  strict_formatting,
const unsigned long  radix_ul 
)

Get the numeric value of a character, assuming that the radix is large enough.

'+' and '-' yield 0.

Parameters
chrthe character to get the numeric value of
char_typethe type to use for characters
typethe type to use for the return value
strict_formattingif true, don't allow upper case characters
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an integer expression of the given type with the numeric value of the char

There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters


return char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0
return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0

Definition at line 627 of file string_constraint_generator_valueof.cpp.

References char_type(), and from_integer().

Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string().

◆ is_digit_with_radix()

exprt is_digit_with_radix ( const exprt chr,
const bool  strict_formatting,
const exprt radix_as_char,
const unsigned long  radix_ul 
)

Check if a character is a digit with respect to the given radix, e.g.

if the radix is 10 then check if the character is in the range 0-9.

Parameters
chrthe character
strict_formattingif true, don't allow upper case characters
radix_as_charthe radix as an expression of the same type as chr
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an expression for the condition

Definition at line 557 of file string_constraint_generator_valueof.cpp.

References char_type(), exprt::copy_to_operands(), from_integer(), PRECONDITION, and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_correct_number_format().

◆ max_printed_string_length()

size_t max_printed_string_length ( const typet type,
unsigned long  radix_ul 
)

Calculate the string length needed to represent any value of the given type using the given radix.

Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.

Parameters
typethe type that we are considering values of
radix_ulthe radix we are using, or 0, in which case the return value will work for any radix
Returns
the maximum string length

We want to calculate max, the maximum number of characters needed to represent any value of the given type.

For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))

For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))

Definition at line 701 of file string_constraint_generator_valueof.cpp.

References bitvector_typet::get_width(), irept::id(), and to_bitvector_type().

Referenced by string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_string_of_int_with_radix(), and string_of_int_builtin_functiont::length_constraint().