cprover
printf_formatter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: printf Formatting
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "printf_formatter.h"
13 
14 #include <cassert>
15 #include <sstream>
16 
17 #include <util/c_types.h>
18 #include <util/format_constant.h>
19 #include <util/simplify_expr.h>
20 
22  const exprt &src, const typet &dest)
23 {
24  if(src.type()==dest)
25  return src;
26  exprt tmp=src;
27  tmp.make_typecast(dest);
28  simplify(tmp, ns);
29  return tmp;
30 }
31 
33  const std::string &_format,
34  const std::list<exprt> &_operands)
35 {
36  format=_format;
37  operands=_operands;
38 }
39 
40 void printf_formattert::print(std::ostream &out)
41 {
42  format_pos=0;
43  next_operand=operands.begin();
44 
45  try
46  {
47  while(!eol()) process_char(out);
48  }
49 
50  catch(eol_exceptiont)
51  {
52  }
53 }
54 
56 {
57  std::ostringstream stream;
58  print(stream);
59  return stream.str();
60 }
61 
62 void printf_formattert::process_format(std::ostream &out)
63 {
64  exprt tmp;
65  format_constantt format_constant;
66 
67  format_constant.precision=6;
68  format_constant.min_width=0;
69  format_constant.zero_padding=false;
70 
71  char ch=next();
72 
73  if(ch=='0') // leading zeros
74  {
75  format_constant.zero_padding=true;
76  ch=next();
77  }
78 
79  while(isdigit(ch)) // width
80  {
81  format_constant.min_width*=10;
82  format_constant.min_width+=ch-'0';
83  ch=next();
84  }
85 
86  if(ch=='.') // precision
87  {
88  format_constant.precision=0;
89  ch=next();
90 
91  while(isdigit(ch))
92  {
93  format_constant.precision*=10;
94  format_constant.precision+=ch-'0';
95  ch=next();
96  }
97  }
98 
99  switch(ch)
100  {
101  case '%':
102  out << ch;
103  break;
104 
105  case 'e':
106  case 'E':
107  format_constant.style=format_spect::stylet::SCIENTIFIC;
108  if(next_operand==operands.end())
109  break;
110  out << format_constant(
112  break;
113 
114  case 'f':
115  case 'F':
116  format_constant.style=format_spect::stylet::DECIMAL;
117  if(next_operand==operands.end())
118  break;
119  out << format_constant(
121  break;
122 
123  case 'g':
124  case 'G':
125  format_constant.style=format_spect::stylet::AUTOMATIC;
126  if(format_constant.precision==0)
127  format_constant.precision=1;
128  if(next_operand==operands.end())
129  break;
130  out << format_constant(
132  break;
133 
134  case 's':
135  {
136  if(next_operand==operands.end())
137  break;
138  // this is the address of a string
139  const exprt &op=*(next_operand++);
140  if(op.id()==ID_address_of &&
141  op.operands().size()==1 &&
142  op.op0().id()==ID_index &&
143  op.op0().operands().size()==2 &&
144  op.op0().op0().id()==ID_string_constant)
145  out << format_constant(op.op0().op0());
146  }
147  break;
148 
149  case 'd':
150  if(next_operand==operands.end())
151  break;
152  out << format_constant(
154  break;
155 
156  case 'D':
157  if(next_operand==operands.end())
158  break;
159  out << format_constant(
161  break;
162 
163  case 'u':
164  if(next_operand==operands.end())
165  break;
166  out << format_constant(
168  break;
169 
170  case 'U':
171  if(next_operand==operands.end())
172  break;
173  out << format_constant(
175  break;
176 
177  default:
178  out << '%' << ch;
179  }
180 }
181 
182 void printf_formattert::process_char(std::ostream &out)
183 {
184  char ch=next();
185 
186  if(ch=='%')
187  process_format(out);
188  else
189  out << ch;
190 }
The type of an expression.
Definition: type.h:22
exprt & op0()
Definition: expr.h:72
stylet style
Definition: format_spec.h:28
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
void process_char(std::ostream &out)
bitvector_typet double_type()
Definition: c_types.cpp:193
typet & type()
Definition: expr.h:56
printf Formatting
std::list< exprt >::const_iterator next_operand
const irep_idt & id() const
Definition: irep.h:259
std::list< exprt > operands
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
const namespacet & ns
unsigned precision
Definition: format_spec.h:19
bool zero_padding
Definition: format_spec.h:20
unsigned min_width
Definition: format_spec.h:18
Base class for all expressions.
Definition: expr.h:42
void process_format(std::ostream &out)
void print(std::ostream &out)
void operator()(const std::string &format, const std::list< exprt > &_operands)
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
operandst & operands()
Definition: expr.h:66
void make_typecast(const typet &_type)
Definition: expr.cpp:84
std::string as_string()
const exprt make_type(const exprt &src, const typet &dest)
bool simplify(exprt &expr, const namespacet &ns)