CBMC
format_constant.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "format_constant.h"
11 
12 #include "arith_tools.h"
13 #include "fixedbv.h"
14 #include "ieee_float.h"
15 #include "std_expr.h"
16 #include "string_constant.h"
17 
18 std::string format_constantt::operator()(const exprt &expr)
19 {
20  if(expr.is_constant())
21  {
22  if(expr.type().id()==ID_natural ||
23  expr.type().id()==ID_integer ||
24  expr.type().id()==ID_unsignedbv ||
25  expr.type().id()==ID_signedbv)
26  {
27  mp_integer i;
28  if(to_integer(to_constant_expr(expr), i))
29  return "(number conversion failed)";
30 
31  return integer2string(i);
32  }
33  else if(expr.type().id()==ID_fixedbv)
34  {
35  return fixedbvt(to_constant_expr(expr)).format(*this);
36  }
37  else if(expr.type().id()==ID_floatbv)
38  {
39  return ieee_floatt(to_constant_expr(expr)).format(*this);
40  }
41  }
42  else if(expr.id()==ID_string_constant)
43  return id2string(to_string_constant(expr).value());
44 
45  return "(format-constant failed: "+expr.id_string()+")";
46 }
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
std::string format(const format_spect &format_spec) const
Definition: fixedbv.cpp:134
std::string operator()(const exprt &expr)
std::string format(const format_spect &format_spec) const
Definition: ieee_float.cpp:70
const std::string & id_string() const
Definition: irep.h:387
const irep_idt & id() const
Definition: irep.h:384
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
BigInt mp_integer
Definition: smt_terms.h:17
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const string_constantt & to_string_constant(const exprt &expr)