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 #include <util/std_expr.h>
20 
22  const exprt &src, const typet &dest)
23 {
24  if(src.type()==dest)
25  return src;
26  return simplify_expr(typecast_exprt(src, dest), ns);
27 }
28 
30  const std::string &_format,
31  const std::list<exprt> &_operands)
32 {
33  format=_format;
34  operands=_operands;
35 }
36 
37 void printf_formattert::print(std::ostream &out)
38 {
39  format_pos=0;
40  next_operand=operands.begin();
41 
42  try
43  {
44  while(!eol()) process_char(out);
45  }
46 
47  catch(const eol_exceptiont &)
48  {
49  }
50 }
51 
53 {
54  std::ostringstream stream;
55  print(stream);
56  return stream.str();
57 }
58 
59 void printf_formattert::process_format(std::ostream &out)
60 {
61  exprt tmp;
62  format_constantt format_constant;
63 
64  format_constant.precision=6;
65  format_constant.min_width=0;
66  format_constant.zero_padding=false;
67 
68  char ch=next();
69 
70  if(ch=='0') // leading zeros
71  {
72  format_constant.zero_padding=true;
73  ch=next();
74  }
75 
76  while(isdigit(ch)) // width
77  {
78  format_constant.min_width*=10;
79  format_constant.min_width+=ch-'0';
80  ch=next();
81  }
82 
83  if(ch=='.') // precision
84  {
85  format_constant.precision=0;
86  ch=next();
87 
88  while(isdigit(ch))
89  {
90  format_constant.precision*=10;
91  format_constant.precision+=ch-'0';
92  ch=next();
93  }
94  }
95 
96  switch(ch)
97  {
98  case '%':
99  out << ch;
100  break;
101 
102  case 'e':
103  case 'E':
104  format_constant.style=format_spect::stylet::SCIENTIFIC;
105  if(next_operand==operands.end())
106  break;
107  out << format_constant(
109  break;
110 
111  case 'f':
112  case 'F':
113  format_constant.style=format_spect::stylet::DECIMAL;
114  if(next_operand==operands.end())
115  break;
116  out << format_constant(
118  break;
119 
120  case 'g':
121  case 'G':
122  format_constant.style=format_spect::stylet::AUTOMATIC;
123  if(format_constant.precision==0)
124  format_constant.precision=1;
125  if(next_operand==operands.end())
126  break;
127  out << format_constant(
129  break;
130 
131  case 's':
132  {
133  if(next_operand==operands.end())
134  break;
135  // this is the address of a string
136  const exprt &op=*(next_operand++);
137  if(
138  op.id() == ID_address_of &&
139  to_address_of_expr(op).object().id() == ID_index &&
140  to_index_expr(to_address_of_expr(op).object()).array().id() ==
141  ID_string_constant)
142  {
143  out << format_constant(
144  to_index_expr(to_address_of_expr(op).object()).array());
145  }
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 }
printf_formattert::as_string
std::string as_string()
Definition: printf_formatter.cpp:52
format_spect::stylet::DECIMAL
@ DECIMAL
printf_formattert::next
char next()
Definition: printf_formatter.h:46
printf_formatter.h
printf Formatting
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
format_spect::zero_padding
bool zero_padding
Definition: format_spec.h:20
exprt
Base class for all expressions.
Definition: expr.h:53
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:21
printf_formattert::print
void print(std::ostream &out)
Definition: printf_formatter.cpp:37
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:81
printf_formattert::operator()
void operator()(const std::string &format, const std::list< exprt > &_operands)
Definition: printf_formatter.cpp:29
printf_formattert::ns
const namespacet & ns
Definition: printf_formatter.h:37
format_constantt
Definition: format_constant.h:20
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
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
format_spect::min_width
unsigned min_width
Definition: format_spec.h:18
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
irept::id
const irep_idt & id() const
Definition: irep.h:418
format_spect::stylet::SCIENTIFIC
@ 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:182
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
format_spect::precision
unsigned precision
Definition: format_spec.h:19
format_spect::stylet::AUTOMATIC
@ AUTOMATIC
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
printf_formattert::eol_exceptiont
Definition: printf_formatter.h:44
std_expr.h
API to expression classes.
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:59