Frama-C Bug Tracking System - Frama-C
View Issue Details
0001004Frama-CPlug-in > jessiepublic2011-10-27 17:102013-03-27 09:44
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001004: Jessie reports syntax error in .mlw file
DescriptionInvoking frama-c -jessie -pp-annot cc.c on the attached file produces:

Error while reading file '../cc.mlw':
File "cc/../cc.mlw", line 4342, characters 10-13:
syntax error
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f cc.makefile why3ml

This file did verify with the previous version of Frama-C/Jessie/alt-ergo+simplify.
TagsNo tags attached.
Attached Filesc cc.c (12,157) 2011-10-27 17:10

2011-10-28 06:57   
I see, the reason is that the "val" identifier is a keyword in Why3 and Jessie did not take this into account.

A quick work-around is to rename the variable 'val' in your code

Fixed in Why SVN Nitrogen branch
2013-03-27 09:43   
Fixed in Frama-C Oxygen + Why 2.32.

Issue History
2011-10-27 17:10borisNew Issue
2011-10-27 17:10borisStatusnew => assigned
2011-10-27 17:10borisAssigned To => cmarche
2011-10-27 17:10borisFile Added: cc.c
2011-10-28 06:57cmarcheNote Added: 0002432
2011-10-28 06:58cmarcheStatusassigned => resolved
2011-10-28 06:58cmarcheResolutionopen => fixed
2013-03-27 09:43signolesNote Added: 0003782
2013-03-27 09:44signolesFixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44signolesStatusresolved => closed