CBMC
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/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 {
34  format=_format;
35  operands=_operands;
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()) process_char(out);
46  }
47 
48  catch(const eol_exceptiont &)
49  {
50  }
51 }
52 
54 {
55  std::ostringstream stream;
56  print(stream);
57  return stream.str();
58 }
59 
60 void printf_formattert::process_format(std::ostream &out)
61 {
62  exprt tmp;
63  format_constantt format_constant;
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':
105  format_constant.style=format_spect::stylet::SCIENTIFIC;
106  if(next_operand==operands.end())
107  break;
108  out << format_constant(
110  break;
111 
112  case 'f':
113  case 'F':
114  format_constant.style=format_spect::stylet::DECIMAL;
115  if(next_operand==operands.end())
116  break;
117  out << format_constant(
119  break;
120 
121  case 'g':
122  case 'G':
123  format_constant.style=format_spect::stylet::AUTOMATIC;
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 &&
140  to_address_of_expr(op).object().id() == ID_index &&
141  to_index_expr(to_address_of_expr(op).object()).array().id() ==
142  ID_string_constant)
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 
183 void 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 }
printf_formattert::as_string
std::string as_string()
Definition: printf_formatter.cpp:53
format_spect::stylet::DECIMAL
@ DECIMAL
printf_formattert::next
char next()
Definition: printf_formatter.h:45
printf_formatter.h
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:380
typet
The type of an expression, extends irept.
Definition: type.h:28
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1478
format_spect::zero_padding
bool zero_padding
Definition: format_spec.h:20
exprt
Base class for all expressions.
Definition: expr.h:55
printf_formattert::eol
bool eol() const
Definition: printf_formatter.h:41
printf_formattert::make_type
const exprt make_type(const exprt &src, const typet &dest)
Definition: printf_formatter.cpp:22
printf_formattert::print
void print(std::ostream &out)
Definition: printf_formatter.cpp:38
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:104
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
printf_formattert::operator()
void operator()(const std::string &format, const std::list< exprt > &_operands)
Definition: printf_formatter.cpp:30
printf_formattert::ns
const namespacet & ns
Definition: printf_formatter.h:36
format_constantt
Definition: format_constant.h:19
printf_formattert::operands
std::list< exprt > operands
Definition: printf_formatter.h:38
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
format_spect::min_width
unsigned min_width
Definition: format_spec.h:18
pointer_expr.h
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2931
index_exprt::array
exprt & array()
Definition: std_expr.h:1440
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
irept::id
const irep_idt & id() const
Definition: irep.h:396
format_spect::stylet::SCIENTIFIC
@ SCIENTIFIC
printf_formattert::format
std::string format
Definition: printf_formatter.h:37
format_spect::style
stylet style
Definition: format_spec.h:28
double_type
floatbv_typet double_type()
Definition: c_types.cpp:203
simplify_expr.h
format_constant.h
printf_formattert::next_operand
std::list< exprt >::const_iterator next_operand
Definition: printf_formatter.h:39
printf_formattert::process_char
void process_char(std::ostream &out)
Definition: printf_formatter.cpp:183
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:90
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:408
format_spect::precision
unsigned precision
Definition: format_spec.h:19
format_spect::stylet::AUTOMATIC
@ AUTOMATIC
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2016
printf_formattert::eol_exceptiont
Definition: printf_formatter.h:43
std_expr.h
printf_formattert::format_pos
unsigned format_pos
Definition: printf_formatter.h:40
c_types.h
printf_formattert::process_format
void process_format(std::ostream &out)
Definition: printf_formatter.cpp:60