cprover
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 <sstream>
15
16#include <util/c_types.h>
18#include <util/pointer_expr.h>
19#include <util/simplify_expr.h>
20#include <util/std_expr.h>
21
23 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
38void printf_formattert::print(std::ostream &out)
39{
40 format_pos=0;
41 next_operand=operands.begin();
42
43 try
44 {
45 while(!eol()) process_char(out);
46 }
47
48 catch(const eol_exceptiont &)
49 {
50 }
51}
52
54{
55 std::ostringstream stream;
57 return stream.str();
58}
59
60void printf_formattert::process_format(std::ostream &out)
61{
62 exprt tmp;
64
65 format_constant.precision=6;
66 format_constant.min_width=0;
67 format_constant.zero_padding=false;
68
69 char ch=next();
70
71 if(ch=='0') // leading zeros
72 {
73 format_constant.zero_padding=true;
74 ch=next();
75 }
76
77 while(isdigit(ch)) // width
78 {
79 format_constant.min_width*=10;
80 format_constant.min_width+=ch-'0';
81 ch=next();
82 }
83
84 if(ch=='.') // precision
85 {
86 format_constant.precision=0;
87 ch=next();
88
89 while(isdigit(ch))
90 {
91 format_constant.precision*=10;
92 format_constant.precision+=ch-'0';
93 ch=next();
94 }
95 }
96
97 switch(ch)
98 {
99 case '%':
100 out << ch;
101 break;
102
103 case 'e':
104 case 'E':
106 if(next_operand==operands.end())
107 break;
108 out << format_constant(
110 break;
111
112 case 'f':
113 case 'F':
115 if(next_operand==operands.end())
116 break;
117 out << format_constant(
119 break;
120
121 case 'g':
122 case 'G':
124 if(format_constant.precision==0)
125 format_constant.precision=1;
126 if(next_operand==operands.end())
127 break;
128 out << format_constant(
130 break;
131
132 case 's':
133 {
134 if(next_operand==operands.end())
135 break;
136 // this is the address of a string
137 const exprt &op=*(next_operand++);
138 if(
139 op.id() == ID_address_of &&
141 to_index_expr(to_address_of_expr(op).object()).array().id() ==
143 {
144 out << format_constant(
145 to_index_expr(to_address_of_expr(op).object()).array());
146 }
147 }
148 break;
149
150 case 'd':
151 if(next_operand==operands.end())
152 break;
153 out << format_constant(
155 break;
156
157 case 'D':
158 if(next_operand==operands.end())
159 break;
160 out << format_constant(
162 break;
163
164 case 'u':
165 if(next_operand==operands.end())
166 break;
167 out << format_constant(
169 break;
170
171 case 'U':
172 if(next_operand==operands.end())
173 break;
174 out << format_constant(
176 break;
177
178 default:
179 out << '%' << ch;
180 }
181}
182
183void printf_formattert::process_char(std::ostream &out)
184{
185 char ch=next();
186
187 if(ch=='%')
188 process_format(out);
189 else
190 out << ch;
191}
signedbv_typet signed_long_int_type()
Definition c_types.cpp:90
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:54
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:104
signedbv_typet signed_int_type()
Definition c_types.cpp:40
floatbv_typet double_type()
Definition c_types.cpp:203
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
exprt & array()
Definition std_expr.h:1353
const irep_idt & id() const
Definition irep.h:396
std::list< exprt > operands
const exprt make_type(const exprt &src, const typet &dest)
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)
void print(std::ostream &out)
const namespacet & ns
void process_char(std::ostream &out)
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
printf Formatting
exprt simplify_expr(exprt src, const namespacet &ns)
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391