Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000256Frama-CPlug-in > jessiepublic2009-09-25 14:302009-09-25 14:59
Reporterjcrown 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000256: array range in requires predicate
Descriptionframa-c -main foo file.c -jessie on code typedef struct { int a; } A; typedef struct { A * c[10]; } B; typedef struct { B * c[10]; } C; C v; /*@.......*/ void foo(void); wth one of the 3 contracts below on foo() /*@ requires \valid((v.c[0 .. 9])->c[0 .. 9]); */ /*@ requires \valid((v.c[0 .. 9])->c+(0 .. 9)); */ /*@ requires \valid((v.c+(0 .. 9))->c+(0 .. 9)); */ -> Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed on the 1st and 2nd ones, and file.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c on the 3rd one.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-09-25 14:30 jcrown New Issue
2009-09-25 14:59 signoles Status new => assigned
2009-09-25 14:59 signoles Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker