145 std::vector<string_constraint_generatort::format_specifiert>
fspec;
155 static bool check_format_string(std::string s)
157 std::string format_specifier=
158 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
159 std::regex regex(format_specifier);
162 while(std::regex_search(s, match, regex))
164 if(match.position()!= 0)
165 for(
const auto &c : match.str())
171 for(
const auto &c : s)
189 int index=m[1].str().empty()?-1:std::stoi(m[1].str());
190 std::string flag=m[2].str().empty()?
"":m[2].str();
191 int width=m[3].str().empty()?-1:std::stoi(m[3].str());
192 int precision=m[4].str().empty()?-1:std::stoi(m[4].str());
193 std::string tT=m[5].str();
201 m[6].str().length()==1,
"format conversion should be one character");
202 char conversion=m[6].str()[0];
205 index, flag, width, precision, dt, conversion);
215 std::string format_specifier=
216 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
217 std::regex regex(format_specifier);
218 std::vector<format_elementt> al;
221 while(std::regex_search(s, match, regex))
223 if(match.position()!=0)
225 std::string pre_match=s.substr(0, match.position());
226 al.emplace_back(pre_match);
338 false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
351 const std::string &s,
355 std::vector<array_string_exprt> intermediary_strings;
356 std::size_t arg_count=0;
362 if(fe.is_format_specifier())
372 arg_count<args.size(),
"number of format must match specifiers");
379 static_cast<std::size_t>(fs.
index)<=args.size(),
380 "number of format must match specifiers");
386 intermediary_strings.push_back(
392 const exprt return_code =
394 intermediary_strings.push_back(str);
400 if(intermediary_strings.empty())
408 if(intermediary_strings.size() == 1)
416 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
437 std::wstring out(length,
'?');
439 for(std::size_t i=0; i<arr.
operands().size() && i<length; i++)
444 INVARIANT(!conversion_failed,
"constant should be convertible to unsigned");
469 if(
s1.length().id()==ID_constant &&
470 s1.content().id()==ID_array &&
482 <<
"ignoring format function with non constant first argument"
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
const signedbv_typet get_return_code_type()
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
exprt add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr)
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 s...
static mstreamt & eom(mstreamt &m)
format_textt(std::string _content)
#define INVARIANT(CONDITION, REASON)
mstreamt & warning() const
exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
exprt 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.
format_textt(const format_textt &fs)
API to expression classes.
exprt add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String...
#define PRECONDITION(CONDITION)
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic 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 a generic exprt to a struct_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
std::vector< exprt > operandst
exprt 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(st...
Base class for all expressions.
std::size_t component_number(const irep_idt &component_name) const
exprt add_axioms_from_bool(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(Z) java function.
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
exprt add_axioms_for_format(const function_application_exprt &f)
Formatted string using a format string and list of arguments.
std::vector< exprt > lemmas
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
struct constructor from list of elements
bitvector_typet char_type()
exprt 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.
array constructor from list of elements
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
std::string get_content() const
array_string_exprt add_axioms_for_format_specifier(const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type)
Parse s and add axioms ensuring the output corresponds to the output of String.format.