Jessie/GWhy/Gappa: format file and invalid POs proved valid
ID0000046: This issue was created automatically from Mantis Issue 46. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000046 | Frama-C | Plug-in > jessie | public | 2009-04-10 | 2009-06-23 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Beryllium-20090601-beta1 |
Description :
Hello,
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.0x ); }
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