Why keywords as ACSL identifiers
ID0000391: This issue was created automatically from Mantis Issue 391. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000391 | Frama-C | Plug-in > jessie | public | 2010-02-03 | 2010-04-19 |
| Reporter | signoles | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
The generated why file contains a syntax error (a keyword is used where an identifier is expected).
Additional Information :
Fixed in Why CVS
Steps To Reproduce :
=== t.c === /*@ lemma rec: \true; */
$ frama-c -jessie t.c File "why/t.why", line 94, characters 5-8: Syntax error