CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
format_specifier.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Format specifiers for String.format
4
5Author: Romain Brenguier, Joel Allred
6
7Date: June 2019
8
9\*******************************************************************/
10
13
14#include "format_specifier.h"
15#include <regex>
16
25{
26 PRECONDITION(m.size() == 7);
27 int index = m[1].str().empty() ? -1 : std::stoi(m[1].str());
28 std::string flag = m[2].str();
29 int width = m[3].str().empty() ? -1 : std::stoi(m[3].str());
30 int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str());
31 // `tT` values: "t" = date/time, "T" = uppercase date/time
32 std::string tT = m[5].str();
33
34 // date/time
35 bool dt = !tT.empty();
36 if(tT == "T")
38
40 m[6].str().length() == 1, "format conversion should be one character");
41 char conversion = m[6].str()[0];
42
43 return format_specifiert(index, flag, width, precision, dt, conversion);
44}
45
48std::vector<format_elementt> parse_format_string(std::string s)
49{
50 const std::string format_specifier =
51 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
52 std::regex regex(format_specifier);
53 std::vector<format_elementt> al;
54 std::smatch match;
55
56 while(std::regex_search(s, match, regex))
57 {
58 if(match.position() != 0)
59 {
60 std::string pre_match = s.substr(0, match.position());
61 al.emplace_back(pre_match);
62 }
63
64 al.emplace_back(format_specifier_of_match(match));
65 s = match.suffix();
66 }
67
68 al.emplace_back(s);
69 return al;
70}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
static const char DATE_TIME_UPPER
static format_specifiert format_specifier_of_match(std::smatch &m)
Helper function for parsing format strings.
std::vector< format_elementt > parse_format_string(std::string s)
Regexp is taken directly from openJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9...
Format specifiers for String.format.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423