Frama-C Bug Tracking System - Frama-C
View Issue Details
0000222Frama-CPlug-in > jessiepublic2009-08-27 17:272009-11-03 16:55
bobot 
cmarche 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Beryllium-20090902 
0000222: Recursive logic definitions are not correctly translated.
The 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
id : 6016
No tags attached.
Issue History
2009-08-27 17:27bobotNew Issue
2009-08-28 05:06signolesStatusnew => assigned
2009-08-28 05:06signolesAssigned To => cmarche
2009-11-03 16:51cmarcheNote Added: 0000514
2009-11-03 16:51cmarcheStatusassigned => resolved
2009-11-03 16:51cmarcheResolutionopen => fixed
2009-11-03 16:55signolesStatusresolved => closed
2009-11-03 16:55signolesFixed in Version => Frama-C Beryllium 2

Notes
(0000514)
cmarche   
2009-11-03 16:51   
Apparently already fixed in Why 2.21