Skip to content

Commit 7ba5ac4

Browse files
tautschnigtautschnig
committed
Support length modifiers in printf formatting
Handle all length modifiers and conversion specifiers as laid out in printf's man page. Fixes: #7147
1 parent e5ac52d commit 7ba5ac4

File tree

3 files changed

+166
-27
lines changed

3 files changed

+166
-27
lines changed

‎regression/cbmc/printf3/main.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
#include <stdio.h>
3+
4+
int main()
5+
{
6+
printf("%ld", 10);
7+
printf("%llu", 11);
8+
printf("%hhd", 12);
9+
printf("%lf", 10.0);
10+
printf("%Lf", 11.0);
11+
assert(0);
12+
}

‎regression/cbmc/printf3/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE no-new-smt
2+
main.c
3+
--trace
4+
^10$
5+
^11$
6+
^12$
7+
^10.0+$
8+
^11.0+$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring

‎src/goto-programs/printf_formatter.cpp

+142-27
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,15 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "printf_formatter.h"
1313

14-
#include <sstream>
15-
1614
#include <util/c_types.h>
15+
#include <util/expr_util.h>
1716
#include <util/format_constant.h>
1817
#include <util/pointer_expr.h>
1918
#include <util/simplify_expr.h>
2019
#include <util/std_expr.h>
2120

21+
#include <sstream>
22+
2223
const exprt printf_formattert::make_type(
2324
const exprt &src, const typet &dest)
2425
{
@@ -66,6 +67,8 @@ void printf_formattert::process_format(std::ostream &out)
6667
format_constant.min_width=0;
6768
format_constant.zero_padding=false;
6869

70+
std::string length_modifier;
71+
6972
char ch=next();
7073

7174
if(ch=='0') // leading zeros
@@ -94,6 +97,56 @@ void printf_formattert::process_format(std::ostream &out)
9497
}
9598
}
9699

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+
97150
switch(ch)
98151
{
99152
case '%':
@@ -105,17 +158,23 @@ void printf_formattert::process_format(std::ostream &out)
105158
format_constant.style=format_spect::stylet::SCIENTIFIC;
106159
if(next_operand==operands.end())
107160
break;
108-
out << format_constant(
109-
make_type(*(next_operand++), double_type()));
161+
if(length_modifier == "L")
162+
out << format_constant(make_type(*(next_operand++), long_double_type()));
163+
else
164+
out << format_constant(make_type(*(next_operand++), double_type()));
110165
break;
111166

167+
case 'a': // TODO: hexadecimal output
168+
case 'A': // TODO: hexadecimal output
112169
case 'f':
113170
case 'F':
114171
format_constant.style=format_spect::stylet::DECIMAL;
115172
if(next_operand==operands.end())
116173
break;
117-
out << format_constant(
118-
make_type(*(next_operand++), double_type()));
174+
if(length_modifier == "L")
175+
out << format_constant(make_type(*(next_operand++), long_double_type()));
176+
else
177+
out << format_constant(make_type(*(next_operand++), double_type()));
119178
break;
120179

121180
case 'g':
@@ -125,10 +184,14 @@ void printf_formattert::process_format(std::ostream &out)
125184
format_constant.precision=1;
126185
if(next_operand==operands.end())
127186
break;
128-
out << format_constant(
129-
make_type(*(next_operand++), double_type()));
187+
if(length_modifier == "L")
188+
out << format_constant(make_type(*(next_operand++), long_double_type()));
189+
else
190+
out << format_constant(make_type(*(next_operand++), double_type()));
130191
break;
131192

193+
case 'S':
194+
length_modifier = 'l';
132195
case 's':
133196
{
134197
if(next_operand==operands.end())
@@ -153,35 +216,87 @@ void printf_formattert::process_format(std::ostream &out)
153216
break;
154217

155218
case 'd':
219+
case 'i':
220+
{
156221
if(next_operand==operands.end())
157222
break;
158-
out << format_constant(
159-
make_type(*(next_operand++), signed_int_type()));
223+
typet conversion_type;
224+
if(length_modifier == "hh")
225+
conversion_type = signed_char_type();
226+
else if(length_modifier == "h")
227+
conversion_type = signed_short_int_type();
228+
else if(length_modifier == "l")
229+
conversion_type = signed_long_int_type();
230+
else if(length_modifier == "ll")
231+
conversion_type = signed_long_long_int_type();
232+
else if(length_modifier == "j") // intmax_t
233+
conversion_type = signed_long_long_int_type();
234+
else if(length_modifier == "z")
235+
conversion_type = signed_size_type();
236+
else if(length_modifier == "t")
237+
conversion_type = pointer_diff_type();
238+
else
239+
conversion_type = signed_int_type();
240+
out << format_constant(make_type(*(next_operand++), conversion_type));
241+
}
160242
break;
161243

162-
case 'D':
163-
if(next_operand==operands.end())
164-
break;
165-
out << format_constant(
166-
make_type(*(next_operand++), signed_long_int_type()));
244+
case 'o': // TODO: octal output
245+
case 'x': // TODO: hexadecimal output
246+
case 'X': // TODO: hexadecimal output
247+
case 'u':
248+
{
249+
if(next_operand == operands.end())
250+
break;
251+
typet conversion_type;
252+
if(length_modifier == "hh")
253+
conversion_type = unsigned_char_type();
254+
else if(length_modifier == "h")
255+
conversion_type = unsigned_short_int_type();
256+
else if(length_modifier == "l")
257+
conversion_type = unsigned_long_int_type();
258+
else if(length_modifier == "ll")
259+
conversion_type = unsigned_long_long_int_type();
260+
else if(length_modifier == "j") // intmax_t
261+
conversion_type = unsigned_long_long_int_type();
262+
else if(length_modifier == "z")
263+
conversion_type = size_type();
264+
else if(length_modifier == "t")
265+
conversion_type = pointer_diff_type();
266+
else
267+
conversion_type = unsigned_int_type();
268+
out << format_constant(make_type(*(next_operand++), conversion_type));
269+
}
167270
break;
168271

169-
case 'u':
170-
if(next_operand==operands.end())
272+
case 'C':
273+
length_modifier = 'l';
274+
case 'c':
275+
if(next_operand == operands.end())
276+
break;
277+
if(length_modifier == "l")
278+
out << format_constant(make_type(*(next_operand++), wchar_t_type()));
279+
else
280+
out << format_constant(
281+
make_type(*(next_operand++), unsigned_char_type()));
171282
break;
172-
out << format_constant(
173-
make_type(*(next_operand++), unsigned_int_type()));
174-
break;
175283

176-
case 'U':
177-
if(next_operand==operands.end())
284+
case 'p':
285+
// TODO: hexadecimal output
286+
out << format_constant(make_type(*(next_operand++), size_type()));
178287
break;
179-
out << format_constant(
180-
make_type(*(next_operand++), unsigned_long_int_type()));
181-
break;
182288

183-
default:
184-
out << '%' << ch;
289+
case 'n':
290+
if(next_operand == operands.end())
291+
break;
292+
// printf would store the number of characters written so far in the
293+
// object pointed to by this operand. We do not implement this side-effect
294+
// here, and just skip one operand.
295+
++next_operand;
296+
break;
297+
298+
default:
299+
out << '%' << ch;
185300
}
186301
}
187302

0 commit comments

Comments
 (0)