144 std::vector<format_specifiert>
fspec;
154 static bool check_format_string(std::string s)
156 std::string format_specifier=
157 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
158 std::regex regex(format_specifier);
161 while(std::regex_search(s, match, regex))
163 if(match.position()!= 0)
164 for(
const auto &c : match.str())
170 for(
const auto &c : s)
187 int index=m[1].str().empty()?-1:std::stoi(m[1].str());
188 std::string flag=m[2].str().empty()?
"":m[2].str();
189 int width=m[3].str().empty()?-1:std::stoi(m[3].str());
190 int precision=m[4].str().empty()?-1:std::stoi(m[4].str());
191 std::string tT=m[5].str();
198 m[6].str().length()==1,
"format conversion should be one character");
199 char conversion=m[6].str()[0];
211 std::string format_specifier=
212 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
213 std::regex regex(format_specifier);
214 std::vector<format_elementt> al;
217 while(std::regex_search(s, match, regex))
219 if(match.position()!=0)
221 std::string pre_match=s.substr(0, match.position());
222 al.emplace_back(pre_match);
259 static std::pair<array_string_exprt, string_constraintst>
272 std::pair<exprt, string_constraintst> return_code;
278 return {res, std::move(return_code.second)};
282 return {res, std::move(return_code.second)};
290 return {res, std::move(return_code.second)};
298 return {res, std::move(return_code.second)};
302 return {res, std::move(return_code.second)};
306 return {res, std::move(return_code.second)};
314 return {res, std::move(return_code.second)};
318 return {res, std::move(return_code.second)};
321 return {res, std::move(return_code.second)};
343 const exprt return_code_upper_case =
346 return_code_upper_case, res, format_specifier_result.first);
347 auto upper_case_constraints = upper_case_function.
constraints(fresh_symbol);
348 merge(upper_case_constraints, std::move(format_specifier_result.second));
349 return {res, std::move(upper_case_constraints)};
367 false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
384 const std::string &s,
392 std::vector<array_string_exprt> intermediary_strings;
393 std::size_t arg_count=0;
399 if(fe.is_format_specifier())
409 arg_count<args.size(),
"number of format must match specifiers");
416 static_cast<std::size_t>(fs.
index)<=args.size(),
417 "number of format must match specifiers");
425 merge(constraints, std::move(result.second));
426 intermediary_strings.push_back(result.first);
434 merge(constraints, result.second);
435 intermediary_strings.push_back(str);
441 if(intermediary_strings.empty())
445 return {return_code, constraints};
450 if(intermediary_strings.size() == 1)
455 merge(constraints, std::move(result.second));
456 return {result.first, std::move(constraints)};
460 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
466 return_code =
maximum(return_code, result.first);
467 merge(constraints, std::move(result.second));
473 merge(constraints, std::move(result.second));
474 return {
maximum(result.first, return_code), std::move(constraints)};
485 for(
const auto &op : arr.
operands())
488 std::wstring out(length,
'?');
490 for(std::size_t i=0; i<arr.
operands().size() && i<length; i++)
522 if(
s1.length().id() == ID_constant &&
s1.content().id() == ID_array)
531 fresh_symbol, res, s, args, array_pool, message, ns);
536 <<
"ignoring format function with non constant first argument"
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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.
The type of an expression, extends irept.
Generates string constraints to link results from string functions with their arguments.
Application of (mathematical) function.
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::pair< exprt, string_constraintst > add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
String representation of a float value.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Generation of fresh symbols of a given type.
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
typet & type()
Return the type of the expression.
signedbv_typet get_return_code_type()
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Structure type, corresponds to C style structs.
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
format_textt(std::string _content)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
mstreamt & warning() const
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, 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,...
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
format_textt(const format_textt &fs)
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
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.
Class that provides messages with a built-in verbosity 'level'.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::vector< exprt > operandst
exprt maximum(const exprt &a, const exprt &b)
std::vector< exprt > existential
std::pair< exprt, string_constraintst > 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.
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Base class for all expressions.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
const typet & subtype() const
Struct constructor from list of elements.
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms to write the float in scientific notation.
bitvector_typet char_type()
Array constructor from list of elements.
std::string get_content() const