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