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