cprover
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 "expr.h"
14 #include "fixedbv.h"
15 #include "ieee_float.h"
16 #include "std_expr.h"
17 #include "string_constant.h"
18 
19 std::string format_constantt::operator()(const exprt &expr)
20 {
21  if(expr.is_constant())
22  {
23  if(expr.type().id()==ID_natural ||
24  expr.type().id()==ID_integer ||
25  expr.type().id()==ID_unsignedbv ||
26  expr.type().id()==ID_signedbv)
27  {
28  mp_integer i;
29  if(to_integer(to_constant_expr(expr), i))
30  return "(number conversion failed)";
31 
32  return integer2string(i);
33  }
34  else if(expr.type().id()==ID_fixedbv)
35  {
36  return fixedbvt(to_constant_expr(expr)).format(*this);
37  }
38  else if(expr.type().id()==ID_floatbv)
39  {
40  return ieee_floatt(to_constant_expr(expr)).format(*this);
41  }
42  }
43  else if(expr.id()==ID_string_constant)
44  return id2string(to_string_constant(expr).get_value());
45 
46  return "(format-constant failed: "+expr.id_string()+")";
47 }
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:19
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
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:65
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const string_constantt & to_string_constant(const exprt &expr)