cprover
|
Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/simplify_expr.h>
#include <util/deprecate.h>
#include <cmath>
#include <solvers/floatbv/float_bv.h>
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... | |
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.
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.
res | string expression for the result |
i | an integer argument |
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().
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.
chr | the character to get the numeric value of |
char_type | the type to use for characters |
type | the type to use for the return value |
strict_formatting | if true, don't allow upper case characters |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
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().
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.
chr | the character |
strict_formatting | if true, don't allow upper case characters |
radix_as_char | the radix as an expression of the same type as chr |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
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().
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.
type | the type that we are considering values of |
radix_ul | the radix we are using, or 0, in which case the return value will work for any radix |
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().