Go to the documentation of this file.
29 const exprt &return_code,
30 const std::vector<exprt> &fun_args,
41 .map([&](
const exprt &arg) {
44 "arguments of format should be strings");
47 .collect<std::vector<array_string_exprt>>();
52 format_string_expr.
content().
id() == ID_array)
54 const auto length = numeric_cast_v<std::size_t>(
68 static bool check_format_string(std::string s)
70 std::string format_specifier=
71 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
72 std::regex regex(format_specifier);
75 while(std::regex_search(s, match, regex))
77 if(match.position()!= 0)
78 for(
const auto &c : match.str())
84 for(
const auto &c : s)
116 static std::pair<array_string_exprt, string_constraintst>
128 std::pair<exprt, string_constraintst> return_code;
134 return {res, std::move(return_code.second)};
141 return {res, std::move(return_code.second)};
145 return {res, std::move(return_code.second)};
149 return {res, std::move(return_code.second)};
156 const exprt is_null_literal =
is_null(string_expr, array_pool);
171 return {res, constraints};
176 return {res, std::move(return_code.second)};
179 const exprt arg_string = string_arg;
181 return {std::move(string_expr), {}};
186 return {res, std::move(return_code.second)};
190 return {res, std::move(return_code.second)};
193 return {res, std::move(return_code.second)};
208 const exprt return_code_upper_case =
211 return_code_upper_case, res, format_specifier_result.first, array_pool);
212 auto upper_case_constraints =
214 merge(upper_case_constraints, std::move(format_specifier_result.second));
215 return {res, std::move(upper_case_constraints)};
231 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
246 if(
id ==
"string_expr")
294 const std::string &s,
295 const std::vector<array_string_exprt> &args,
301 std::vector<array_string_exprt> intermediary_strings;
302 std::size_t arg_count = 0;
310 if(fe.is_format_specifier())
321 arg_count < args.size(),
"number of format must match specifiers");
322 string_arg = args[arg_count++];
328 static_cast<std::size_t
>(fs.
index) <= args.size(),
329 "number of format must match specifiers");
332 string_arg = args[fs.
index - 1];
338 merge(constraints, std::move(result.second));
339 intermediary_strings.push_back(result.first);
346 str, fe.get_format_text().get_content());
347 merge(constraints, result.second);
348 intermediary_strings.push_back(str);
354 if(intermediary_strings.empty())
358 return {return_code, constraints};
363 if(intermediary_strings.size() == 1)
371 merge(constraints, std::move(result.second));
372 return {result.first, std::move(constraints)};
376 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
382 return_code =
maximum(return_code, result.first);
383 merge(constraints, std::move(result.second));
389 merge(constraints, std::move(result.second));
390 return {
maximum(result.first, return_code), std::move(constraints)};
394 const std::vector<mp_integer> serialized,
400 for(std::size_t i = 0; i < 4; i++)
403 serialized[i] <= 0xFFFF,
404 "Component of serialized value to"
405 "format must be bounded by 0xFFFF");
408 const int64_t int64_value =
409 (serialized[0] << 48).to_long() | (serialized[1] << 32).to_long() |
410 (serialized[2] << 16).to_long() | serialized[3].to_long();
411 const mp_integer mp_integer_value{int64_value};
412 const std::string long_as_string =
integer2string(mp_integer_value, base);
419 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
420 string[2] ==
'l' &&
string[3] ==
'l';
427 const std::vector<mp_integer> &arg)
434 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
440 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
444 if(
'A' <= c && c <=
'Z')
452 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
462 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
463 return std::vector<mp_integer>{arg[3]};
468 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
469 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
477 return std::vector<mp_integer>{
'\n'};
479 return std::vector<mp_integer>{
'%'};
494 if(
'a' <= c && c <=
'z')
510 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
514 const std::function<
exprt(
const exprt &)> &get_value)
const
519 const std::vector<format_elementt> format_strings =
521 std::vector<mp_integer> result_vector;
522 std::size_t arg_count = 0;
526 if(fe.is_format_specifier())
533 std::vector<mp_integer> evaluated_char_vector;
538 arg_count <
inputs.size(),
539 "number of format must match specifiers");
549 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
550 "number of format must match specifiers");
559 evaluated_char_vector.begin(),
560 evaluated_char_vector.end(),
561 std::back_inserter(result_vector));
565 result_vector.push_back(
'%');
571 result_vector.push_back(
'\n');
576 for(
char c : fe.get_format_text().get_content())
577 result_vector.emplace_back(c);
600 "add_axioms_for_format should return 0, meaning that formatting was"
602 result_constraint_pair.second.existential.push_back(
604 return result_constraint_pair.second;
623 const exprt &pos_integer,
625 const typet &length_type,
626 const unsigned long radix)
640 pos_integer, max_length - 1, length_type, radix),
651 const exprt &integer,
652 const typet &length_type,
653 const unsigned long radix)
655 int max_pos_int_length;
659 max_pos_int_length = 10;
661 max_pos_int_length = 8;
674 integer, max_pos_int_length, length_type, radix),
730 const exprt arg_string =
762 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
771 const std::vector<format_elementt> format_strings =
773 std::vector<exprt> intermediary_string_lengths;
774 std::size_t arg_count = 0;
779 if(fe.is_format_specifier())
790 arg_count <
inputs.size(),
791 "number of format must match specifiers");
792 arg =
inputs[arg_count++];
798 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
799 "number of format must match specifiers");
805 intermediary_string_lengths.push_back(
818 if(intermediary_string_lengths.empty())
825 exprt total_length = intermediary_string_lengths[0];
826 for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
829 plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
832 std::move(total_length)});
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & length_type() const
const typet & subtype() const
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
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,...
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
The type of an expression, extends irept.
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
Fixed-width bit-vector with IEEE floating-point interpretation.
symbol_generatort fresh_symbol
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 get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
The plus expression Associativity is not specified.
Base class for all expressions.
Collection of constraints of different types: existential formulas, universal formulas,...
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
bitvector_typet index_type()
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Fixed-width bit-vector with unsigned binary interpretation.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
typet & type()
Return the type of the expression.
exprt maximum(const exprt &a, const exprt &b)
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
Fixed-width bit-vector with two's complement interpretation.
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
exprt simplify_expr(exprt src, const namespacet &ns)
The unary minus expression.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
The Boolean constant false.
array_string_exprt & to_array_string_expr(exprt &expr)
nonstd::optional< T > optionalt
signedbv_typet get_return_code_type()
Base class for string functions that are built in the solver.
bitvector_typet char_type()
bool is_zero() const
Return whether the expression is a constant representing 0.
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.
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 ...
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool is_refined_string_type(const typet &type)
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
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....
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_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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Semantic type conversion.
The Boolean constant true.
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....
binary_relation_exprt less_than(exprt lhs, exprt rhs)
ranget< iteratort > make_range(iteratort begin, iteratort end)
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
std::vector< exprt > existential
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)