--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on December 2009 ---
[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



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