CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/printf_formatter.cpp Source File

CBMC
Loading...
Searching...
No Matches
printf_formatter.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: printf Formatting
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "printf_formatter.h"
13
14#include <util/c_types.h>
15#include <util/expr_util.h>
16#include <util/format_constant.h>
17#include <util/pointer_expr.h>
18#include <util/simplify_expr.h>
19#include <util/std_expr.h>
20
21#include <sstream>
22
23 const exprt printf_formattert::make_type(const exprt &src, const typet &dest)
24{
25 if(src.type() == dest)
26 return src;
27 return simplify_expr(typecast_exprt(src, dest), ns);
28}
29
31 const std::string &_format,
32 const std::list<exprt> &_operands)
33{
36}
37
38 void printf_formattert::print(std::ostream &out)
39{
40 format_pos = 0;
41 next_operand = operands.begin();
42
43 try
44 {
45 while(!eol())
46 process_char(out);
47 }
48
49 catch(const eol_exceptiont &)
50 {
51 }
52}
53
55{
56 std::ostringstream stream;
57 print(stream);
58 return stream.str();
59}
60
61 void printf_formattert::process_format(std::ostream &out)
62{
63 exprt tmp;
65
66 format_constant.precision = 6;
67 format_constant.min_width = 0;
68 format_constant.zero_padding = false;
69
70 std::string length_modifier;
71
72 char ch = next();
73
74 if(ch == '0') // leading zeros
75 {
76 format_constant.zero_padding = true;
77 ch = next();
78 }
79
80 while(isdigit(ch)) // width
81 {
82 format_constant.min_width *= 10;
83 format_constant.min_width += ch - '0';
84 ch = next();
85 }
86
87 if(ch == '.') // precision
88 {
89 format_constant.precision = 0;
90 ch = next();
91
92 while(isdigit(ch))
93 {
94 format_constant.precision *= 10;
95 format_constant.precision += ch - '0';
96 ch = next();
97 }
98 }
99
100 switch(ch)
101 {
102 case 'h':
103 ch = next();
104 if(ch == 'h')
105 {
106 length_modifier = "hh";
107 ch = next();
108 }
109 else
110 {
111 length_modifier = "h";
112 }
113 break;
114
115 case 'l':
116 ch = next();
117 if(ch == 'l')
118 {
119 length_modifier = "ll";
120 ch = next();
121 }
122 else
123 {
124 length_modifier = "l";
125 }
126 break;
127
128 case 'q':
129 ch = next();
130 length_modifier = "ll";
131 break;
132
133 case 'L':
134 case 'j':
135 case 'z':
136 case 't':
137 length_modifier = ch;
138 ch = next();
139 break;
140
141 case 'Z':
142 ch = next();
143 length_modifier = "z";
144 break;
145
146 default:
147 break;
148 }
149
150 switch(ch)
151 {
152 case '%':
153 out << ch;
154 break;
155
156 case 'e':
157 case 'E':
159 if(next_operand == operands.end())
160 break;
161 if(length_modifier == "L")
163 else
165 break;
166
167 case 'a': // TODO: hexadecimal output
168 case 'A': // TODO: hexadecimal output
169 case 'f':
170 case 'F':
172 if(next_operand == operands.end())
173 break;
174 if(length_modifier == "L")
176 else
178 break;
179
180 case 'g':
181 case 'G':
183 if(format_constant.precision == 0)
184 format_constant.precision = 1;
185 if(next_operand == operands.end())
186 break;
187 if(length_modifier == "L")
189 else
191 break;
192
193 case 'S':
194 length_modifier = 'l';
195 case 's':
196 {
197 if(next_operand == operands.end())
198 break;
199 // this is the address of a string
200 const exprt &op = *(next_operand++);
201 if(
202 auto pointer_constant =
204 {
205 if(
207 skip_typecast(pointer_constant->symbolic_pointer())))
208 {
209 if(address_of->object().id() == ID_string_constant)
210 {
211 out << format_constant(address_of->object());
212 }
213 else if(
214 auto index_expr =
216 {
217 if(
218 index_expr->index() == 0 &&
219 index_expr->array().id() == ID_string_constant)
220 {
221 out << format_constant(index_expr->array());
222 }
223 }
224 }
225 }
226 }
227 break;
228
229 case 'd':
230 case 'i':
231 {
232 if(next_operand == operands.end())
233 break;
235 if(length_modifier == "hh")
237 else if(length_modifier == "h")
239 else if(length_modifier == "l")
241 else if(length_modifier == "ll")
243 else if(length_modifier == "j") // intmax_t
245 else if(length_modifier == "z")
247 else if(length_modifier == "t")
249 else
252 }
253 break;
254
255 case 'o': // TODO: octal output
256 case 'x': // TODO: hexadecimal output
257 case 'X': // TODO: hexadecimal output
258 case 'u':
259 {
260 if(next_operand == operands.end())
261 break;
263 if(length_modifier == "hh")
265 else if(length_modifier == "h")
267 else if(length_modifier == "l")
269 else if(length_modifier == "ll")
271 else if(length_modifier == "j") // intmax_t
273 else if(length_modifier == "z")
275 else if(length_modifier == "t")
277 else
280 }
281 break;
282
283 case 'C':
284 length_modifier = 'l';
285 case 'c':
286 if(next_operand == operands.end())
287 break;
288 if(length_modifier == "l")
290 else
291 out << format_constant(
293 break;
294
295 case 'p':
296 // TODO: hexadecimal output
298 break;
299
300 case 'n':
301 if(next_operand == operands.end())
302 break;
303 // printf would store the number of characters written so far in the
304 // object pointed to by this operand. We do not implement this side-effect
305 // here, and just skip one operand.
306 ++next_operand;
307 break;
308
309 default:
310 out << '%' << ch;
311 }
312}
313
314 void printf_formattert::process_char(std::ostream &out)
315{
316 char ch = next();
317
318 if(ch == '%')
319 process_format(out);
320 else
321 out << ch;
322}
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
signedbv_typet signed_char_type()
Definition c_types.cpp:134
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition c_types.cpp:93
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
signedbv_typet signed_int_type()
Definition c_types.cpp:22
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:127
signedbv_typet signed_size_type()
Definition c_types.cpp:66
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
bitvector_typet wchar_t_type()
Definition c_types.cpp:141
floatbv_typet long_double_type()
Definition c_types.cpp:193
floatbv_typet double_type()
Definition c_types.cpp:185
signedbv_typet signed_short_int_type()
Definition c_types.cpp:29
unsignedbv_typet unsigned_short_int_type()
Definition c_types.cpp:43
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Base class for all expressions.
Definition expr.h:57
typet & type()
Return the type of the expression.
Definition expr.h:85
@ AUTOMATIC
@ DECIMAL
@ SCIENTIFIC
std::list< exprt > operands
const exprt make_type(const exprt &src, const typet &dest)
std::string format
unsigned format_pos
char next()
std::list< exprt >::const_iterator next_operand
std::string as_string()
void operator()(const std::string &format, const std::list< exprt > &_operands)
void process_format(std::ostream &out)
bool eol() const
void print(std::ostream &out)
const namespacet & ns
void process_char(std::ostream &out)
Semantic type conversion.
Definition std_expr.h:1995
The type of an expression, extends irept.
Definition type.h:29
int isdigit(int c)
Definition ctype.c:24
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition expr_util.cpp:188
Deprecated expression utility functions.
API to expression classes for Pointers.
printf Formatting
exprt simplify_expr(exprt src, const namespacet &ns)
API to expression classes.
#define size_type
Definition unistd.c:186

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