Unterminated comment while generating division-by-zero assertion
ID0002250: This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002250 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Linux | OS | Gentoo | OS Version | - |
| Product Version | Frama-C Magnesium | Target Version | Frama-C 14-Silicon | Fixed in Version | - |
Description :
For the following code snippet:
... ret = dividend / *p; ...
RTE generates annotation: /*@ assert rte: signed_overflow: dividend/*p ≤ 2147483647; */
The above leads to unterminated comment preprocessing error
Steps To Reproduce :
frama-c -rte -then -print of the following program:
int zero_division_006_gbl_divisor = 0; void zero_division_006 () { int dividend = 1000; int *p; int ret; p = &zero_division_006_gbl_divisor; ret = dividend / *p; }
int main(int argc, const char **argv) { zero_division_006(); return 0; }