44 DEPRECATED(
"should use add_axioms_from_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_from_int_with_radix(
53 res, f.arguments()[2], f.arguments()[3]);
55 return add_axioms_from_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,
147 const exprt &input_int,
151 PRECONDITION(max_size < std::numeric_limits<size_t>::max());
158 CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
163 CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
169 const bool strict_formatting=
true;
172 input_int, res, radix_as_char, radix_ul, max_size, strict_formatting);
207 DEPRECATED(
"use add_axioms_from_int which takes a radix argument instead")
212 const typet &type=i.type();
225 and_exprt(res.axiom_for_length_gt(0), res.axiom_for_length_le(max_size)));
227 for(
size_t size=1; size<=max_size; size++)
233 for(
size_t j=0; j<size; j++)
236 exprt chr_int = int_of_hex_char(chr);
248 equal_exprt premise(res.axiom_for_has_length(size));
319 const exprt &input_int,
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;
543 const exprt &expr,
unsigned long def)
560 const bool strict_formatting,
561 const exprt &radix_as_char,
562 const unsigned long radix_ul)
564 PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
568 const and_exprt is_digit_when_radix_le_10(
571 chr, ID_lt,
plus_exprt(zero_char, radix_as_char)));
573 if(radix_ul<=10 && radix_ul!=0)
575 return is_digit_when_radix_le_10;
583 const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
592 chr, ID_lt,
plus_exprt(a_char, radix_minus_ten))));
594 if(!strict_formatting)
601 chr, ID_lt,
plus_exprt(A_char, radix_minus_ten))));
608 is_digit_when_radix_le_10,
609 is_digit_when_radix_gt_10);
613 return is_digit_when_radix_gt_10;
632 const bool strict_formatting,
633 const unsigned long radix_ul)
640 chr, ID_ge, zero_char);
642 if(radix_ul<=10 && radix_ul!=0)
647 upper_case_lower_case_or_digit,
660 if(strict_formatting)
669 upper_case_lower_case_or_digit,
684 upper_case_or_lower_case,
687 upper_case_lower_case_or_digit,
709 double radix=
static_cast<double>(radix_ul);
710 bool signed_type=type.
id()==ID_signedbv;
729 double max=signed_type?
730 floor(static_cast<double>(n_bits-1)/log2(radix))+2.0:
731 ceil(static_cast<double>(n_bits)/log2(radix));
732 return static_cast<size_t>(max);
The type of an expression.
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
exprt add_axioms_from_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 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)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal...
const irep_idt & id() const
The boolean constant true.
division (integer and real)
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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
#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)
void add_axioms_for_correct_number_format(const exprt &input_int, 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...
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