_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, 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_type.cpp

@@ -1029,6 +1029,13 @@ void c_typecheck_baset::typecheck_compound_body(
   {
     if(it->id()==ID_static_assert)
     {
+      if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+      {
+        error().source_location = it->source_location();
+        error() << "static_assert not supported in compound body" << eom;
+        throw 0;
+      }
+
       exprt &assertion = to_binary_expr(*it).op0();
       typecheck_expr(assertion);
       typecheck_expr(to_binary_expr(*it).op1());

src/ansi-c/scanner.l

@@ -852,7 +852,15 @@ or_eq               { return cpp98_keyword(TOK_ORASSIGN); }
 private             { return cpp98_keyword(TOK_PRIVATE); }
 protected           { return cpp98_keyword(TOK_PROTECTED); }
 public              { return cpp98_keyword(TOK_PUBLIC); }
-static_assert       { return cpp11_keyword(TOK_STATIC_ASSERT); } // C++11
+static_assert       { // C++11, but Visual Studio supports it in all modes (and
+                      // doesn't support _Static_assert)
+                      if(PARSER.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+                      {
+                        loc(); return TOK_STATIC_ASSERT;
+                      }
+                      else
+                        return cpp11_keyword(TOK_STATIC_ASSERT);
+                    }
 template            { return cpp98_keyword(TOK_TEMPLATE); }
 this                { return cpp98_keyword(TOK_THIS); }
 thread_local        { return cpp11_keyword(TOK_THREAD_LOCAL); } // C++11