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 - 2018 MantisBT Team
Powered by Mantis Bugtracker