cprover
cpp_typecheck_static_assert.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #include <util/std_types.h>
15 
17 {
18  typecheck_expr(cpp_static_assert.op0());
19  typecheck_expr(cpp_static_assert.op1());
20 
21  cpp_static_assert.op0().make_typecast(bool_typet());
22  make_constant(cpp_static_assert.op0());
23 
24  if(cpp_static_assert.op0().is_true())
25  {
26  // ok
27  }
28  else if(cpp_static_assert.op0().is_false())
29  {
30  // failed
31  error().source_location=cpp_static_assert.source_location();
32  error() << "static assertion failed";
33  if(cpp_static_assert.op1().id()==ID_string_constant)
34  error() << ": " << cpp_static_assert.op1().get(ID_value);
35  error() << eom;
36  throw 0;
37  }
38  else
39  {
40  // not true or false
41  error().source_location=cpp_static_assert.source_location();
42  error() << "static assertion is not constant" << eom;
43  throw 0;
44  }
45 }
exprt & op0()
Definition: expr.h:84
virtual void make_constant(exprt &expr)
bool is_false() const
Definition: expr.cpp:140
bool is_true() const
Definition: expr.cpp:133
The proper Booleans.
Definition: std_types.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void typecheck_expr(exprt &expr)
void convert(cpp_linkage_spect &)
const irep_idt & id() const
Definition: irep.h:189
source_locationt source_location
Definition: message.h:175
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
C++ Language Type Checking.
API to type classes.
const source_locationt & source_location() const
Definition: expr.h:142
mstreamt & error()
Definition: message.h:223
void make_typecast(const typet &_type)
Definition: expr.cpp:90