--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Support of (shift) operations?



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