CBMC
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/string_constant.h>
15 
17 {
18  typecheck_expr(cpp_static_assert.op0());
19  typecheck_expr(cpp_static_assert.op1());
20 
21  implicit_typecast_bool(cpp_static_assert.op0());
22  make_constant(cpp_static_assert.op0());
23 
24  if(cpp_static_assert.op0().is_false())
25  {
26  // failed
27  error().source_location=cpp_static_assert.source_location();
28  error() << "static assertion failed";
29  if(cpp_static_assert.op1().id()==ID_string_constant)
30  error() << ": "
31  << to_string_constant(cpp_static_assert.op1()).get_value();
32  error() << eom;
33  throw 0;
34  }
35 }
cpp_typecheckt::convert
void convert(cpp_linkage_spect &)
Definition: cpp_typecheck_linkage_spec.cpp:14
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:40
string_constant.h
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:43
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:4394
messaget::error
mstreamt & error() const
Definition: message.h:399
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:118
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
irept::id
const irep_idt & id() const
Definition: irep.h:396
cpp_typecheck.h
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2263
cpp_static_assertt
Definition: cpp_static_assert.h:17
binary_exprt::op1
exprt & op1()
Definition: expr.h:128
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:211
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:21
binary_exprt::op0
exprt & op0()
Definition: expr.h:125