Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001004Frama-CPlug-in > jessiepublic2011-10-27 17:102013-03-27 09:44
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 file icon cc.c [^] (12,157 bytes) 2011-10-27 17:10 [Show Content]

- Relationships

-  Notes
(0002432)
cmarche (developer)
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
(0003782)
signoles (manager)
2013-03-27 09:43

Fixed in Frama-C Oxygen + Why 2.32.

- Issue History
Date Modified Username Field Change
2011-10-27 17:10 boris New Issue
2011-10-27 17:10 boris Status new => assigned
2011-10-27 17:10 boris Assigned To => cmarche
2011-10-27 17:10 boris File Added: cc.c
2011-10-28 06:57 cmarche Note Added: 0002432
2011-10-28 06:58 cmarche Status assigned => resolved
2011-10-28 06:58 cmarche Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003782
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker