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>
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)};
227 message.
warning() <<
"unimplemented format specifier: " <<
fs.conversion
232 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
248 if(
id ==
"string_expr")
296 const std::string &s,
297 const std::vector<array_string_exprt> &args,
312 if(
fe.is_format_specifier())
323 arg_count < args.size(),
"number of format must match specifiers");
328 INVARIANT(
fs.index > 0,
"index in format should be positive");
330 static_cast<std::size_t
>(
fs.index) <= args.size(),
331 "number of format must match specifiers");
340 merge(constraints, std::move(result.second));
348 str,
fe.get_format_text().get_content());
349 merge(constraints, result.second);
360 return {return_code, constraints};
373 merge(constraints, std::move(result.second));
374 return {result.first, std::move(constraints)};
384 return_code =
maximum(return_code, result.first);
385 merge(constraints, std::move(result.second));
391 merge(constraints, std::move(result.second));
392 return {
maximum(result.first, return_code), std::move(constraints)};
402 for(std::size_t
i = 0;
i < 4;
i++)
406 "Component of serialized value to"
407 "format must be bounded by 0xFFFF");
421 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
422 string[2] ==
'l' &&
string[3] ==
'l';
429 const std::vector<mp_integer> &arg)
431 switch(
fs.conversion)
436 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
442 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
446 if(
'A' <=
c &&
c <=
'Z')
454 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
464 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
465 return std::vector<mp_integer>{arg[3]};
470 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
471 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
479 return std::vector<mp_integer>{
'\n'};
481 return std::vector<mp_integer>{
'%'};
496 if(
'a' <=
c &&
c <=
'z')
512 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
516 const std::function<
exprt(
const exprt &)> &get_value)
const
528 if(
fe.is_format_specifier())
541 "number of format must match specifiers");
549 INVARIANT(
fs.index > 0,
"index in format should be positive");
551 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
552 "number of format must match specifiers");
578 for(
char c :
fe.get_format_text().get_content())
602 "add_axioms_for_format should return 0, meaning that formatting was"
627 const typet &length_type,
628 const unsigned long radix)
654 const typet &length_type,
655 const unsigned long radix)
691 switch(
fs.conversion)
764 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
781 if(
fe.is_format_specifier())
793 "number of format must match specifiers");
798 INVARIANT(
fs.index > 0,
"index in format should be positive");
800 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
801 "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 index_type()
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.
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.
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
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.
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
Fixed-width bit-vector with unsigned binary interpretation.
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'.
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)
optionalt< 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)