Recursive logic definitions are not correctly translated.
ID0000222: This issue was created automatically from Mantis Issue 222. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000222 | Frama-C | Plug-in > jessie | public | 2009-08-27 | 2009-11-03 |
| Reporter | bobot | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Beryllium-20090902 |
Description :
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
Additional Information :
id : 6016