Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices

  • Subject: [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Mon, 7 Dec 2009 21:26:45 +0100
Hello,

we experience a discrepancy between the verification results in the  Jessie-GUI versus those of the command line.
(I am talking about Beryllium-20090901 with why version 2.19 on Mac OS X.)
When verifying the following function.

/*@
  requires \valid(p);
  requires \valid(q);

  assigns *p;
  assigns *q;

  ensures *p == \old(*q);
  ensures *q == \old(*p);
*/
void swap(int* p, int* q)
{
  int save = *p;
  *p = *q;
  *q = save;
}

The results of the command line 

	frama-c -jessie  -jessie-no-regions -jessie-atp yices sw.c

yields
 ...
total   :   6
valid   :   6 (100%)
...
total wallclock time : 0.78 sec

However, when calling the gui with 

	frama-c -jessie  -jessie-no-regions sw.c

we obtain a timeout ("scissors") on the third precondition.

I cannot understand why there  is a timeout in the gui when the total wallclock time for yices is less than a second.
Can other people confirm this on their respective installations?

Regards

Jens Gerlach