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