Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000342Frama-CKernel > ACSL implementationpublic2009-11-23 15:382014-02-12 16:55
Reporternrousset 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000342: Assertion failed instead of typing error report
DescriptionIn the example below, I forgot the parentheses in the expression
(&x[i])->i1 in annotations:

----------------------------------------
typedef struct { int i1; int i2; } s;

/*@ requires
  @ \valid(x + i) && &x[i]->i1 != 0;
  @*/
int f (s x[], int i) {
  return 1 / (&x[i])->i1;
}
-----------------------------------------

It crashes with
assertion failed in cil/src/cil.ml line 2044
instead of reporting a typing error.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000573)
monate (reporter)
2009-11-23 19:11

Thanks for the report. The error will be in the next release:

 tests/cil/bts342.c:6:[kernel] user error: Error during annotations analysis: type s is not a pointer type
 [kernel] user error: skipping file "tests/cil/bts342.c" that has errors.
 [kernel] Plugin kernel aborted because of invalid user input(s).

- Issue History
Date Modified Username Field Change
2009-11-23 15:38 nrousset New Issue
2009-11-23 17:57 signoles Status new => assigned
2009-11-23 17:57 signoles Assigned To => virgile
2009-11-23 19:09 svn Checkin
2009-11-23 19:09 svn Status assigned => resolved
2009-11-23 19:09 svn Resolution open => fixed
2009-11-23 19:11 monate Note Added: 0000573
2010-02-05 09:45 signoles Category Kernel => Kernel > ACSL implementation
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker