42DEPRECATED(
SINCE(2017, 10, 5,
"use add_axioms_for_string_of_int instead"))
47 PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
49 array_pool.find(f.arguments()[1], f.arguments()[0]);
50 if(f.arguments().size() == 4)
51 return add_axioms_for_string_of_int_with_radix(
52 res, f.arguments()[2], f.arguments()[3], 0);
54 return add_axioms_for_string_of_int(
res, f.arguments()[2], 0);
63DEPRECATED(
SINCE(2017, 10, 5,
"Java specific, should be implemented in Java"))
85 for(std::size_t i = 0; i <
str_true.length(); i++)
98 for(std::size_t i = 0; i <
str_false.length(); i++)
116std::pair<exprt, string_constraintst>
136std::pair<exprt, string_constraintst>
150 CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
198DEPRECATED(
SINCE(2017, 10, 5,
"use add_axioms_for_string_of_int_with_radix"))
204 const typet &type = i.type();
207 const typet &index_type =
res.length_type();
221 for(
size_t size = 1; size <=
max_size; size++)
227 for(
size_t j = 0; j < size; j++)
243 equal_to(array_pool.get_or_create_length(
res), size);
258std::pair<exprt, string_constraintst>
282 const unsigned long radix_ul,
329 for(std::size_t index = 1; index <
max_size; ++index)
378 const std::size_t max_string_length,
380 const unsigned long radix_ul)
398 for(
size_t size = 2; size <= max_string_length; size++)
425 if(size - 1 >= max_string_length - 2 || radix_ul == 0)
473 PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
475 const std::size_t max_string_length =
478 return {str, radix, radix_ul, max_string_length};
488std::pair<exprt, string_constraintst>
511 args.max_string_length,
524std::pair<exprt, string_constraintst>
540 args.max_string_length,
559 const unsigned long radix_ul)
561 PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
569 if(radix_ul <= 10 && radix_ul != 0)
628 const unsigned long radix_ul)
637 if(radix_ul <= 10 && radix_ul != 0)
704 double radix =
static_cast<double>(radix_ul);
727 return static_cast<size_t>(max);
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bitvector_typet char_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
Application of (mathematical) function.
The trinary if-then-else operator.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
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.
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.
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.
parseint_argumentst unpack_parseint_arguments(const function_application_exprt &f, const typet &target_int_type)
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....
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....
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.
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
symbol_generatort fresh_symbol
Expression to hold a symbol (variable)
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
#define SINCE(year, month, day, msg)
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Generates string constraints to link results from string functions with their arguments.
exprt get_numeric_value_from_character(const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul)
Get the numeric value of a character, assuming that the radix is large enough.
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.
size_t max_printed_string_length(const typet &type, unsigned long ul_radix)
Calculate the string length needed to represent any value of the given type using the given radix.
signedbv_typet get_return_code_type()
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.
static unsigned long to_integer_or_default(const exprt &expr, unsigned long def, const namespacet &ns)
If the expression is a constant expression then we get the value of it as an unsigned long.
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the 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.
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.
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
equal_exprt equal_to(exprt lhs, exprt rhs)
Argument block for parseInt and cousins, common to parseInt itself and CProverString....
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)