_Static_assert failures should be reported in the front-end

We left it to a failing invariant in goto-program conversion to detect a
failing (local) _Static_assert. Global _Static_assert statements were
not verified at all.

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

src/ansi-c/c_typecheck_base.cpp

@@ -627,9 +627,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, [email protected]
 #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());
+
+    code.op0() = typecast_exprt::conditional_cast(code.op0(), bool_typet{});
+    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());