0000046: Jessie/GWhy/Gappa: format file and invalid POs proved valid

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000046

Frama-C

Plug-in > jessie

public

2009-04-10 14:35

2009-06-23 18:03

Reporter

dpariente

Assigned To

cmarche

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000046: Jessie/GWhy/Gappa: format file and invalid POs proved valid

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

Tags

No 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