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] Support of (shift) operations?

  • Subject: [Frama-c-discuss] Support of (shift) operations?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
  • Date: Tue, 14 Feb 2012 14:03:06 +0100 (CET)
Hello,

i'm currently checking a fixpoint-based matrix library in
Frama-C/Nitrogen and it seems to have troubles at the shift operators
(<<, >>). I boiled this down into a test "program":

void TestFunc(void)
{
  /*@assert 1+1 == 2; */
  /*@assert \forall integer x; (x+1) != x;*/
  /*@assert (2 << 0) == 2; */
  /*@assert (1 << 1) == 2; */
  /*@assert \forall integer x; (x >> 2) == (x/4); */
}

Jessie succeeds in prooving all assertions, but the WP plugin can
proove only the first one on its own, and the second one by help of
alt-ergo. The three last ones are not prooved.
As far as alt-ergo is concerned, the problem seems to be missing
axioms for the basic operators in store_ergo.why; i found only the
prototypes

  logic lshift : int,int -> int
  logic rshift : int,int -> int

I could just add the necessary axioms to my installation but refrain
from it: At first, i dislike the idea of using a "patched version"
and second, this gap is so obvious i presume it is intentional.
I actually tried adding lshift axioms and while alt-ergo cracked the
first four asserts on its own it slowed down quite noticably.
It might be possible to add these to WP itself (fol.ml::e_app comes to
mind), but i'm not sure.
Would anybody be so kind to shade a light on this? I do not even know
whether this belongs to the Frama-C or Why3 discussion list.
 
Thanks in advance

    Daniel

F+S Fleckner und Simon Informationstechnik GmbH
Am Kissel 1a
65549 Limburg
Deutschland / Germany

Phone Front Desk +49 (6431) 40 90 1 - 0, Fax - 30 

http://www.FlecSim.de

Sitz der Gesellschaft: D-65549 Limburg
Registergericht: Limburg HRB 1731
Gesch?ftsf?hrer: Dipl.-Ing. Josef Horstk?tter, Dipl.-Ing. Andr? Zeh