44 DEPRECATED(
"should use add_axioms_for_string_of_int instead")
48 PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
50 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
51 if(f.arguments().size() == 4)
52 return add_axioms_for_string_of_int_with_radix(
53 res, f.arguments()[2], f.arguments()[3]);
55 return add_axioms_for_string_of_int(res, f.arguments()[2]);
62 DEPRECATED(
"This is Java specific and should be implemented in Java instead")
68 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
69 return add_axioms_from_bool(res, f.arguments()[2]);
78 DEPRECATED(
"This is Java specific and should be implemented in Java instead")
94 std::string str_true=
"true";
95 implies_exprt a1(eq, res.axiom_for_has_length(str_true.length()));
98 for(std::size_t i=0; i<str_true.length(); i++)
102 lemmas.push_back(a2);
105 std::string str_false=
"false";
107 lemmas.push_back(a3);
109 for(std::size_t i=0; i<str_false.length(); i++)
113 lemmas.push_back(a4);
129 const exprt &input_int,
134 res, input_int, radix, max_size);
148 const exprt &input_int,
152 PRECONDITION(max_size < std::numeric_limits<size_t>::max());
159 CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
164 CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
170 const bool strict_formatting=
true;
173 res, radix_as_char, radix_ul, max_size, strict_formatting);
209 "use add_axioms_for_string_of_int which takes a radix argument instead")
214 const typet &type=i.type();
227 and_exprt(res.axiom_for_length_gt(0), res.axiom_for_length_le(max_size)));
229 for(
size_t size=1; size<=max_size; size++)
235 for(
size_t j=0; j<size; j++)
238 exprt chr_int = int_of_hex_char(chr);
250 equal_exprt premise(res.axiom_for_has_length(size));
321 const exprt &radix_as_char,
322 const unsigned long radix_ul,
323 const std::size_t max_size,
324 const bool strict_formatting)
329 const exprt &chr=str[0];
332 const exprt starts_with_digit=
337 lemmas.push_back(non_empty);
339 if(strict_formatting)
342 const or_exprt correct_first(starts_with_minus, starts_with_digit);
343 lemmas.push_back(correct_first);
349 starts_with_minus, starts_with_digit, starts_with_plus);
350 lemmas.push_back(correct_first);
355 or_exprt(starts_with_minus, starts_with_plus),
357 lemmas.push_back(contains_digit);
365 for(std::size_t index=1; index<max_size; ++index)
371 str[index], strict_formatting, radix_as_char, radix_ul));
372 lemmas.push_back(character_at_index_is_digit);
375 if(strict_formatting)
383 lemmas.push_back(no_leading_zero);
388 lemmas.push_back(no_leading_zero_after_minus);
405 const exprt &input_int,
407 const bool strict_formatting,
409 const std::size_t max_string_length,
411 const unsigned long radix_ul)
420 str[0],
char_type, type, strict_formatting, radix_ul);
428 for(
size_t size=2; size<=max_string_length; size++)
449 str[size-1],
char_type, type, strict_formatting, radix_ul));
455 if(size-1>=max_string_length-2 || radix_ul==0)
460 digit_constraints.push_back(no_overflow);
466 if(!digit_constraints.empty())
504 PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
509 const bool strict_formatting=
false;
542 const exprt &expr,
unsigned long def)
559 const bool strict_formatting,
560 const exprt &radix_as_char,
561 const unsigned long radix_ul)
563 PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
567 const and_exprt is_digit_when_radix_le_10(
570 chr, ID_lt,
plus_exprt(zero_char, radix_as_char)));
572 if(radix_ul<=10 && radix_ul!=0)
574 return is_digit_when_radix_le_10;
582 const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
591 chr, ID_lt,
plus_exprt(a_char, radix_minus_ten))));
593 if(!strict_formatting)
600 chr, ID_lt,
plus_exprt(A_char, radix_minus_ten))));
607 is_digit_when_radix_le_10,
608 is_digit_when_radix_gt_10);
612 return is_digit_when_radix_gt_10;
631 const bool strict_formatting,
632 const unsigned long radix_ul)
639 chr, ID_ge, zero_char);
641 if(radix_ul<=10 && radix_ul!=0)
646 upper_case_lower_case_or_digit,
659 if(strict_formatting)
668 upper_case_lower_case_or_digit,
683 upper_case_or_lower_case,
686 upper_case_lower_case_or_digit,
708 double radix=
static_cast<double>(radix_ul);
709 bool signed_type=type.
id()==ID_signedbv;
728 double max=signed_type?
729 floor(static_cast<double>(n_bits-1)/log2(radix))+2.0:
730 ceil(static_cast<double>(n_bits)/log2(radix));
731 return static_cast<size_t>(max);
The type of an expression.
void add_axioms_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...
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
void 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...
application of (mathematical) function
const signedbv_typet get_return_code_type()
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
void copy_to_operands(const exprt &expr)
equal_exprt axiom_for_has_length(const exprt &rhs) const
The trinary if-then-else operator.
A constant literal expression.
#define CHECK_RETURN(CONDITION)
exprt conjunction(const exprt::operandst &op)
exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
exprt add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
const irep_idt & id() const
The boolean constant true.
division (integer and real)
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...
Fixed-width bit-vector with two's complement interpretation.
exprt add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
exprt add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String...
#define PRECONDITION(CONDITION)
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.
bitvector_typet index_type()
The unary minus expression.
std::size_t get_width() const
std::vector< exprt > operandst
unsigned long to_integer_or_default(const exprt &expr, unsigned long def)
If the expression is a constant expression then we get the value of it as an unsigned long...
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
bool is_number(const typet &type)
Base class for all expressions.
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.
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
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...
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
bitvector_typet char_type()
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
symbol_generatort fresh_symbol