_Static_assert failures should be reported in the front-end #5677
Conversation
tautschnig
requested review from
chrisr-diffblue and
kroening
as code owners
tautschnig
force-pushed
the
static-assert
branch
from
695e6e9 to
f27a803
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5677 +/- ##
===========================================
- Coverage 69.45% 69.45% -0.01%
===========================================
Files 1243 1243
Lines 100620 100639 +19
===========================================
+ Hits 69887 69899 +12
- Misses 30733 30740 +7
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
src/ansi-c/c_typecheck_code.cpp
Outdated
| typecheck_expr(code.op0()); | ||
| typecheck_expr(code.op1()); | ||
|
|
||
| code.op0() = typecast_exprt::conditional_cast(code.op0(), bool_typet{}); |
There was a problem hiding this comment.
That might not work, consider implicit_typecast_bool?
tautschnig
force-pushed
the
static-assert
branch
from
f27a803 to
ce3b355
Compare
|
#5679 needs to be merged first to make CI happy again. |
| @@ -20,9 +20,6 @@ Author: Daniel Kroening, [email protected] | |||
| simplify_exprt::resultt<> | |||
| simplify_exprt::simplify_isinf(const unary_exprt &expr) | |||
| { | |||
| if(expr.op().type().id() != ID_floatbv) | |||
There was a problem hiding this comment.
I would leave that as a PRECONDITION.
There was a problem hiding this comment.
Could do, but would be redundant with to_floatbv_type(expr.type()) that ieee_floatt::from_expr does. I'm happy to add it for clarity, but if so I'd suggest to add it to simplify_isnan and simplify_isnormal as well?
There was a problem hiding this comment.
Yes, please add, the idea being "fail early" and "clarity".
tautschnig
force-pushed
the
static-assert
branch
from
ce3b355 to
f45b6e6
Compare
This isn't necessarily spelled out in the signature of the function, but GCC's documentation states this requirement.
Fail early if simplification encounters non-floatbv operands to these functions. This would have been caught by ieee_floatt::from_expr, but failing early makes diagnosing easier.
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.
tautschnig
force-pushed
the
static-assert
branch
from
f45b6e6 to
d80f750
Compare
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.