--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on February 2012 ---
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