_Static_assert failures should be reported in the front-end

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

@@ -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());
+
+    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;
 

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

src/cpp/cpp_typecheck_static_assert.cpp

@@ -19,15 +19,10 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
   typecheck_expr(cpp_static_assert.op0());
   typecheck_expr(cpp_static_assert.op1());
 
-  cpp_static_assert.op0() =
-    typecast_exprt::conditional_cast(cpp_static_assert.op0(), bool_typet());
+  implicit_typecast_bool(cpp_static_assert.op0());
   make_constant(cpp_static_assert.op0());
 
-  if(cpp_static_assert.op0().is_true())
-  {
-    // ok
-  }
-  else if(cpp_static_assert.op0().is_false())
+  if(cpp_static_assert.op0().is_false())
   {
     // failed
     error().source_location=cpp_static_assert.source_location();
@@ -38,11 +33,4 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
     error() << eom;
     throw 0;
   }
-  else
-  {
-    // not true or false
-    error().source_location=cpp_static_assert.source_location();
-    error() << "static assertion is not constant" << eom;
-    throw 0;
-  }
 }

src/util/simplify_expr_floatbv.cpp

@@ -20,8 +20,7 @@ Author: Daniel Kroening, [email protected]
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isinf(const unary_exprt &expr)
 {
-  if(expr.op().type().id() != ID_floatbv)
-    return unchanged(expr);
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
 
   if(expr.op().is_constant())
   {
@@ -35,6 +34,8 @@ simplify_exprt::simplify_isinf(const unary_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isnan(const unary_exprt &expr)
 {
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
+
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
@@ -47,6 +48,8 @@ simplify_exprt::simplify_isnan(const unary_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isnormal(const unary_exprt &expr)
 {
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
+
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));