Merge pull request #5677 from tautschnig/static-assert

_Static_assert failures should be reported in the front-end

Author: tautschnig

regression/ansi-c/_Static_assert2/global.c

@@ -0,0 +1,5 @@
+_Static_assert(1 == 0, "must fail");
+
+int main()
+{
+}

regression/ansi-c/_Static_assert2/global.desc

@@ -0,0 +1,10 @@
+CORE gcc-only
+global.c
+
+static assertion failed: must fail
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed

regression/ansi-c/_Static_assert2/local.c

@@ -0,0 +1,4 @@
+int main()
+{
+  _Static_assert(1 == 0, "must fail");
+}

regression/ansi-c/_Static_assert2/local.desc

@@ -0,0 +1,10 @@
+CORE gcc-only
+local.c
+
+static assertion failed: must fail
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed

regression/ansi-c/_Static_assert2/not_constant.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int x;
+  _Static_assert(x, "must fail");
+}

regression/ansi-c/_Static_assert2/not_constant.desc

@@ -0,0 +1,10 @@
+CORE gcc-only
+not_constant.c
+
+expected constant expression
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed

regression/cbmc-library/Float_lib1/main.c

@@ -43,10 +43,10 @@ int main()
 
   _Static_assert(__builtin_isnormal(DBL_MIN), "__builtin_isnormal is constant");
 
-  _Static_assert(!__builtin_isinf(0), "__builtin_isinf is constant");
+  _Static_assert(!__builtin_isinf(0.0), "__builtin_isinf is constant");
 
   _Static_assert(
-    __builtin_isinf_sign(0) == 0, "__builtin_isinf_sign is constant");
+    __builtin_isinf_sign(0.0) == 0, "__builtin_isinf_sign is constant");
 
 #endif
 

src/ansi-c/c_typecheck_base.cpp

@@ -634,9 +634,10 @@ void c_typecheck_baset::typecheck_declaration(
 {
   if(declaration.get_is_static_assert())
   {
-    auto &static_assert_expr = to_binary_expr(declaration);
-    typecheck_expr(static_assert_expr.op0());
-    typecheck_expr(static_assert_expr.op1());
+    codet code(ID_static_assert);
+    code.add_source_location() = declaration.source_location();
+    code.operands().swap(declaration.operands());
+    typecheck_code(code);
   }
   else
   {

src/ansi-c/c_typecheck_code.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/expr_initializer.h>
 #include <util/range.h>
+#include <util/string_constant.h>
 
 #include "ansi_c_declaration.h"
 
@@ -102,9 +103,24 @@ void c_typecheck_baset::typecheck_code(codet &code)
   }
   else if(statement==ID_static_assert)
   {
-    assert(code.operands().size()==2);
+    PRECONDITION(code.operands().size() == 2);
+
     typecheck_expr(code.op0());
     typecheck_expr(code.op1());
+
+    implicit_typecast_bool(code.op0());
+    make_constant(code.op0());
+
+    if(code.op0().is_false())
+    {
+      // failed
+      error().source_location = code.find_source_location();
+      error() << "static assertion failed";
+      if(code.op1().id() == ID_string_constant)
+        error() << ": " << to_string_constant(code.op1()).get_value();
+      error() << eom;
+      throw 0;
+    }
   }
   else if(statement==ID_CPROVER_try_catch ||
           statement==ID_CPROVER_try_finally)
@@ -247,7 +263,6 @@ void c_typecheck_baset::typecheck_decl(codet &code)
 
   if(declaration.get_is_static_assert())
   {
-    assert(declaration.operands().size()==2);
     codet new_code(ID_static_assert);
     new_code.add_source_location()=code.source_location();
     new_code.operands().swap(declaration.operands());

src/ansi-c/c_typecheck_expr.cpp

@@ -2457,6 +2457,15 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
+    const exprt &fp_value = expr.arguments().front();
+
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      error().source_location = fp_value.source_location();
+      error() << "non-floating-point argument for " << identifier << eom;
+      throw 0;
+    }
+
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
@@ -2477,6 +2486,13 @@ exprt c_typecheck_baset::do_special_functions(
 
     const exprt &fp_value = expr.arguments().front();
 
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      error().source_location = fp_value.source_location();
+      error() << "non-floating-point argument for " << identifier << eom;
+      throw 0;
+    }
+
     isinf_exprt isinf_expr(fp_value);
     isinf_expr.add_source_location() = source_location;