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 - 2017 MantisBT Team
Powered by Mantis Bugtracker