2021-03-02 03:00 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000342Frama-CKernel > ACSL implementationpublic2014-02-12 16:55
Reporternrousset 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0000573

monate (reporter)

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).
+Notes

-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
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
2013-12-19 01:13 svn Source_changeset_attached => framac master ecc76f67
2014-02-12 16:55 monate Source_changeset_attached => framac stable/neon ecc76f67
+Issue History