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.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