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; } ## Attachments - [a.c](/uploads/fac19dff3e17847ea3277c0a8c3c3fbf/a.c)