Go to the documentation of this file.
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"
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.
#define PRECONDITION(CONDITION)
const typet & subtype() const
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
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,...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
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.
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.
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.
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
Collection of constraints of different types: existential formulas, universal formulas,...
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.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
bitvector_typet index_type()
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Struct constructor from list of elements.
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
Generation of fresh symbols of a given type.
exprt maximum(const exprt &a, const exprt &b)
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
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.
Application of (mathematical) function.
std::vector< exprt > operandst
format_textt(const format_textt &fs)
signedbv_typet get_return_code_type()
bitvector_typet char_type()
format_textt(std::string _content)
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.
std::string get_content() const
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....
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.
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
mstreamt & warning() const
Array constructor from list of elements.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
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.