30 const exprt &return_code,
42 .map([&](
const exprt &arg) {
45 "arguments of format should be strings");
48 .collect<std::vector<array_string_exprt>>();
72 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
76 while(std::regex_search(s, match,
regex))
78 if(match.position()!= 0)
79 for(
const auto &
c : match.str())
85 for(
const auto &
c : s)
117static std::pair<array_string_exprt, string_constraintst>
122 const typet &index_type,
129 std::pair<exprt, string_constraintst> return_code;
130 switch(
fs.conversion)
135 return {
res, std::move(return_code.second)};
142 return {
res, std::move(return_code.second)};
146 return {
res, std::move(return_code.second)};
150 return {
res, std::move(return_code.second)};
172 return {
res, constraints};
177 return {
res, std::move(return_code.second)};
187 return {
res, std::move(return_code.second)};
191 return {
res, std::move(return_code.second)};
194 return {
res, std::move(return_code.second)};
229 message.warning() <<
"unimplemented format specifier: " <<
fs.conversion
236 "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
252 if(
id ==
"string_expr")
300 const std::string &s,
301 const std::vector<array_string_exprt> &args,
310 const typet &index_type =
res.length_type();
316 if(
fe.is_format_specifier())
327 arg_count < args.size(),
"number of format must match specifiers");
332 INVARIANT(
fs.index > 0,
"index in format should be positive");
334 static_cast<std::size_t
>(
fs.index) <= args.size(),
335 "number of format must match specifiers");
344 merge(constraints, std::move(result.second));
352 str,
fe.get_format_text().get_content());
353 merge(constraints, result.second);
364 return {return_code, constraints};
377 merge(constraints, std::move(result.second));
378 return {result.first, std::move(constraints)};
388 return_code =
maximum(return_code, result.first);
389 merge(constraints, std::move(result.second));
395 merge(constraints, std::move(result.second));
396 return {
maximum(result.first, return_code), std::move(constraints)};
406 for(std::size_t i = 0; i < 4; i++)
410 "Component of serialized value to"
411 "format must be bounded by 0xFFFF");
425 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
426 string[2] ==
'l' &&
string[3] ==
'l';
433 const std::vector<mp_integer> &arg)
435 switch(
fs.conversion)
440 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
446 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
450 if(
'A' <=
c &&
c <=
'Z')
458 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
468 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
469 return std::vector<mp_integer>{arg[3]};
474 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
475 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
483 return std::vector<mp_integer>{
'\n'};
485 return std::vector<mp_integer>{
'%'};
500 if(
'a' <=
c &&
c <=
'z')
516 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
520 const std::function<
exprt(
const exprt &)> &get_value)
const
532 if(
fe.is_format_specifier())
545 "number of format must match specifiers");
553 INVARIANT(
fs.index > 0,
"index in format should be positive");
555 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
556 "number of format must match specifiers");
582 for(
char c :
fe.get_format_text().get_content())
601 "add_axioms_for_format should return 0, meaning that formatting was"
626 const typet &length_type,
627 const unsigned long radix)
653 const typet &length_type,
654 const unsigned long radix)
687 const typet &index_type,
690 switch(
fs.conversion)
763 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
780 if(
fe.is_format_specifier())
792 "number of format must match specifiers");
797 INVARIANT(
fs.index > 0,
"index in format should be positive");
799 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
800 "number of format must match specifiers");
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
API to expression classes for bitvectors.
bitvector_typet char_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Correspondance between arrays and pointers string representations.
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 fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
Fixed-width bit-vector with IEEE floating-point interpretation.
The trinary if-then-else operator.
Class that provides messages with a built-in verbosity 'level'.
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
Base class for string functions that are built in the solver.
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
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....
symbol_generatort fresh_symbol
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
Fixed-width bit-vector with unsigned binary interpretation.
double pow(double x, double y)
const std::string integer2string(const mp_integer &n, unsigned base)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool is_refined_string_type(const typet &type)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define UNREACHABLE_BECAUSE(REASON)
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 array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
std::optional< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
signedbv_typet get_return_code_type()
binary_relation_exprt less_than(exprt lhs, exprt rhs)
array_string_exprt & to_array_string_expr(exprt &expr)
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
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)