Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002250Frama-CKernelpublic2016-10-13 18:122016-12-05 20:30
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformLinuxOSGentooOS Version
Product VersionFrama-C Magnesium 
Target VersionFrama-C 14-SiliconFixed in Version 
Summary0002250: Unterminated comment while generating division-by-zero assertion
DescriptionFor 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 Reproduceframa-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; }
TagsNo tags attached.
Attached Filesc file icon a.c [^] (252 bytes) 2016-10-13 18:12 [Show Content]

- Relationships

-  Notes
(0006271)
signoles (manager)
2016-10-13 18:22

Indeed it is a pretty printer issue. Here is a repro case independent of any plug-in: ===== a.i ===== int A = 1; int main(void) { int *p = &A; /*@ assert A / *p == 1; */ } =============== $ frama-c -print a.i
(0006272)
yakobowski (manager)
2016-10-13 19:49

I propose that we homogenize the pretty-printers of ACSL and of the C part, by putting spaces after binop everywhere.
(0006295)
yakobowski (manager)
2016-12-05 20:26

Fixed in Silicon.
(0006296)
yakobowski (manager)
2016-12-05 20:30

Fixed in Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2016-10-13 18:12 kvorobyov New Issue
2016-10-13 18:12 kvorobyov Status new => assigned
2016-10-13 18:12 kvorobyov Assigned To => signoles
2016-10-13 18:12 kvorobyov File Added: a.c
2016-10-13 18:15 kvorobyov Category Plug-in > E-ACSL => Plug-in > RTE
2016-10-13 18:21 signoles Category Plug-in > RTE => Kernel
2016-10-13 18:22 signoles Note Added: 0006271
2016-10-13 18:22 signoles Status assigned => confirmed
2016-10-13 18:28 signoles Target Version Frama-C GIT, precise the release id => Frama-C 14-Silicon
2016-10-13 18:29 signoles Product Version Frama-C GIT, precise the release id => Frama-C Magnesium
2016-10-13 19:49 yakobowski Note Added: 0006272
2016-12-05 20:26 yakobowski Note Added: 0006295
2016-12-05 20:26 yakobowski Status confirmed => resolved
2016-12-05 20:26 yakobowski Resolution open => fixed
2016-12-05 20:30 yakobowski Status resolved => closed
2016-12-05 20:30 yakobowski Note Added: 0006296


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker