Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000222Frama-CPlug-in > jessiepublic2009-08-27 17:272009-11-03 16:55
Reporterbobot 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000222: Recursive logic definitions are not correctly translated.
DescriptionThe example 2.33 (p44 in acsl-implementation.pdf) is not correctly translated :

/*@ logic integer max_index { L }( int t [] , integer n ) =
  @ ( n ==0) ? 0 :
  @ ( t [n -1]==0) ? n : max_index (t , n -1);
  @*/


# frama-c -jessie max_index.c

File "why/max_index.why", line 158, characters 13-66:
Unbound variable max_index
Additional Informationid : 6016
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000514)
cmarche (developer)
2009-11-03 16:51


Apparently already fixed in Why 2.21

- Issue History
Date Modified Username Field Change
2009-08-27 17:27 bobot New Issue
2009-08-28 05:06 signoles Status new => assigned
2009-08-28 05:06 signoles Assigned To => cmarche
2009-11-03 16:51 cmarche Note Added: 0000514
2009-11-03 16:51 cmarche Status assigned => resolved
2009-11-03 16:51 cmarche Resolution open => fixed
2009-11-03 16:55 signoles Status resolved => closed
2009-11-03 16:55 signoles Fixed in Version => Frama-C Beryllium 2


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker