diff --git a/regression/ansi-c/_Static_assert2/global.c b/regression/ansi-c/_Static_assert2/global.c new file mode 100644 index 00000000000..99bb44ac6f8 --- /dev/null +++ b/regression/ansi-c/_Static_assert2/global.c @@ -0,0 +1,5 @@ +_Static_assert(1 == 0, "must fail"); + +int main() +{ +} diff --git a/regression/ansi-c/_Static_assert2/global.desc b/regression/ansi-c/_Static_assert2/global.desc new file mode 100644 index 00000000000..468a950aadd --- /dev/null +++ b/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 diff --git a/regression/ansi-c/_Static_assert2/local.c b/regression/ansi-c/_Static_assert2/local.c new file mode 100644 index 00000000000..c4e70f51342 --- /dev/null +++ b/regression/ansi-c/_Static_assert2/local.c @@ -0,0 +1,4 @@ +int main() +{ + _Static_assert(1 == 0, "must fail"); +} diff --git a/regression/ansi-c/_Static_assert2/local.desc b/regression/ansi-c/_Static_assert2/local.desc new file mode 100644 index 00000000000..645efb91a3a --- /dev/null +++ b/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 diff --git a/regression/ansi-c/_Static_assert2/not_constant.c b/regression/ansi-c/_Static_assert2/not_constant.c new file mode 100644 index 00000000000..e399e16bbd7 --- /dev/null +++ b/regression/ansi-c/_Static_assert2/not_constant.c @@ -0,0 +1,5 @@ +int main() +{ + int x; + _Static_assert(x, "must fail"); +} diff --git a/regression/ansi-c/_Static_assert2/not_constant.desc b/regression/ansi-c/_Static_assert2/not_constant.desc new file mode 100644 index 00000000000..f619ae94084 --- /dev/null +++ b/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 diff --git a/regression/cbmc-library/Float_lib1/main.c b/regression/cbmc-library/Float_lib1/main.c index 15fefc4583a..7b7ba2981a2 100644 --- a/regression/cbmc-library/Float_lib1/main.c +++ b/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 diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 5c0d114b1ed..cfa58bb6a24 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/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 { diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 480d80b0bb2..1b98556e3e0 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #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()); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 925f67e40e7..3440fcb51bb 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index b107cb73b6d..e89e0cbf215 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/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()); diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 2b45492e515..147518b9f09 100644 --- a/src/ansi-c/scanner.l +++ b/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 diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp index 30aa476bd20..663079dce75 100644 --- a/src/cpp/cpp_typecheck_static_assert.cpp +++ b/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; - } } diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index 28b7278d2cb..5c722f3a060 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -20,8 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com 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()));