CBMC: /home/runner/work/cbmc/cbmc/src/solvers/strings/format_specifier.h Source File

CBMC
Loading...
Searching...
No Matches
format_specifier.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Format specifiers for String.format
4
5Author: Romain Brenguier, Joel Allred
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_SOLVERS_STRINGS_FORMAT_SPECIFIER_H
13#define CPROVER_SOLVERS_STRINGS_FORMAT_SPECIFIER_H
14
15#include <string>
16#include <util/invariant.h>
17#include <vector>
18
19// Format specifier describes how a value should be printed.
23{
24public:
25 // Constants describing the meaning of characters in format specifiers.
26 static const char DECIMAL_INTEGER = 'd';
27 static const char OCTAL_INTEGER = 'o';
28 static const char HEXADECIMAL_INTEGER = 'x';
29 static const char HEXADECIMAL_INTEGER_UPPER = 'X';
30 static const char SCIENTIFIC = 'e';
31 static const char SCIENTIFIC_UPPER = 'E';
32 static const char GENERAL = 'g';
33 static const char GENERAL_UPPER = 'G';
34 static const char DECIMAL_FLOAT = 'f';
35 static const char HEXADECIMAL_FLOAT = 'a';
36 static const char HEXADECIMAL_FLOAT_UPPER = 'A';
37 static const char CHARACTER = 'c';
38 static const char CHARACTER_UPPER = 'C';
39 static const char DATE_TIME = 't';
40 static const char DATE_TIME_UPPER = 'T';
41 static const char BOOLEAN = 'b';
42 static const char BOOLEAN_UPPER = 'B';
43 static const char STRING = 's';
44 static const char STRING_UPPER = 'S';
45 static const char HASHCODE = 'h';
46 static const char HASHCODE_UPPER = 'H';
47 static const char LINE_SEPARATOR = 'n';
48 static const char PERCENT_SIGN = '%';
49
50 int index = -1;
51 std::string flag;
52 int width;
54 // date/time
55 bool dt = false;
57
59 int _index,
60 std::string _flag,
61 int _width,
62 int _precision,
63 bool _dt,
64 char conversion)
65 : index(_index),
66 flag(_flag),
67 width(_width),
69 dt(_dt),
71 {
72 }
73};
74
75// Format text represent a constant part of a format string.
77{
78public:
79 format_textt() = default;
80
81 explicit format_textt(std::string _content) : content(_content)
82 {
83 }
84
88
89 std::string get_content() const
90{
91 return content;
92 }
93
94private:
95 std::string content;
96};
97
98// A format element is either a specifier or text.
100{
101public:
102 typedef enum
103 {
105 TEXT
107
108 explicit format_elementt(format_typet _type) : type(_type)
109 {
110 }
111
112 explicit format_elementt(std::string s) : type(TEXT), fstring(s)
113 {
114 }
115
117 {
118 fspec.push_back(fs);
119 }
120
122{
123 return type == SPECIFIER;
124 }
125
126 bool is_format_text() const
127{
128 return type == TEXT;
129 }
130
132{
134 return fspec.back();
135 }
136
142
144{
146 return fstring;
147 }
148
149private:
152 std::vector<format_specifiert> fspec;
153};
154
160std::vector<format_elementt> parse_format_string(std::string s);
161
162#endif // CPROVER_SOLVERS_STRINGS_FORMAT_SPECIFIER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
format_typet type
format_typet
@ SPECIFIER
@ TEXT
format_elementt(std::string s)
format_elementt(format_typet _type)
format_textt fstring
format_elementt(format_specifiert fs)
format_textt & get_format_text()
bool is_format_text() const
format_specifiert get_format_specifier() const
const format_textt & get_format_text() const
std::vector< format_specifiert > fspec
bool is_format_specifier() const
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
static const char STRING_UPPER
static const char OCTAL_INTEGER
char conversion
static const char SCIENTIFIC
static const char PERCENT_SIGN
static const char DATE_TIME_UPPER
static const char SCIENTIFIC_UPPER
static const char HEXADECIMAL_INTEGER
int precision
static const char DATE_TIME
static const char BOOLEAN_UPPER
format_specifiert(int _index, std::string _flag, int _width, int _precision, bool _dt, char conversion)
static const char STRING
int width
bool dt
static const char CHARACTER
static const char HASHCODE
std::string flag
static const char GENERAL
static const char HEXADECIMAL_INTEGER_UPPER
static const char HASHCODE_UPPER
static const char HEXADECIMAL_FLOAT_UPPER
int index
static const char BOOLEAN
static const char DECIMAL_FLOAT
static const char CHARACTER_UPPER
static const char GENERAL_UPPER
static const char DECIMAL_INTEGER
static const char HEXADECIMAL_FLOAT
static const char LINE_SEPARATOR
std::string get_content() const
format_textt()=default
std::string content
format_textt(std::string _content)
format_textt(const format_textt &fs)
std::vector< format_elementt > parse_format_string(std::string s)
Parse the given string into format specifiers and text.
#define PRECONDITION(CONDITION)
Definition invariant.h:463

AltStyle によって変換されたページ (->オリジナル) /