Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000046Frama-CPlug-in > jessiepublic2009-04-10 14:352009-06-23 18:03
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000046: Jessie/GWhy/Gappa: format file and invalid POs proved valid
DescriptionHello, Under Cygwin, for the following code: /*@ requires -1.0 <= x <= 1.0; assigns \nothing; ensures -1.0 <= \result <= 1.0; */ float f(float x) { return ( -2.0*x ); } with command-line: frama-c -jessie-analysis -jessie-gui faux.c all POs are proved Valid under GWhy, even they are *not*! In GWhy's Debug mode, standard output displays: oblig : f_ensures_default_po_1 calling Gappa on c:\TEMP\gwhyd42d1e_why.gappa command line: gappa < c:\TEMP\gwhyd42d1e_why.gappa Output file c:\TEMP\outba8609: input in flex scanner failed ... Trying to prove the 1st PO through the following command line: gappa c:\TEMP\gwhyd42d1e_why.gappa yields: Error: syntax error, unexpected $undefined at line 1 column 27 1/ It seems that gappa files are expected to be in UNIX format, and not in DOS' one (i.e. with CR/LF ending lines). 2/ When gappa fails in achieving file parsing, GWhy seems to wrongly interpret it as proved Valid. Best regards, Dillon
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000014)
dpariente (reporter)
2009-04-11 17:12

Once cpulimit-win replaced with its last version as mentionned in Bug-0049, point #2 presented here is solved. However, point #1 remains. For information, Gappa version used is 0.11.1.
(0000015)
gmelquio (reporter)
2009-04-14 11:34

I have released Gappa 0.11.2, which should hopefully fix the eol issue.
(0000016)
dpariente (reporter)
2009-04-14 21:38
edited on: 2009-04-14 21:38

Thanks a lot Guillaume! Now the 2 issues identified above are solved. This bug report may be closed.
(0000087)
cmarche (developer)
2009-05-22 15:53

Guillaume melquiond fixed that issue with gappa 0.12 (was a pb with EOL markers under windows)

- Issue History
Date Modified Username Field Change
2009-04-10 14:35 dpariente New Issue
2009-04-10 21:41 signoles Status new => assigned
2009-04-10 21:41 signoles Assigned To => signoles
2009-04-10 21:41 signoles Assigned To signoles => cmarche
2009-04-11 17:12 dpariente Note Added: 0000014
2009-04-14 11:34 gmelquio Note Added: 0000015
2009-04-14 21:38 dpariente Note Added: 0000016
2009-04-14 21:38 dpariente Note Edited: 0000016
2009-05-22 15:53 cmarche Note Added: 0000087
2009-05-22 15:53 cmarche Status assigned => resolved
2009-05-22 15:53 cmarche Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker