--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on February 2012 ---
Hello, Indeed, there is no default axiomatization of logical shifts generated by WP plug-in. Actually, it is difficult to choose a set of complete and "non- expensive" axioms for alt-ergo (you already noticed it). You have two solutions here : - specify your own axioms in ACSL (the easy way) - add external libraries for alt-ergo, why, coq, etc. (using the -wp- why-lib / -wp-coq-lib options) of WP 0.5 Considering new axioms for alt-ergo, you must pay attention to *triggers* ; otherwise, the solver may try to apply the lemmas too often, possibly making the exploration state too large and slowing down the process. By the way, there is no way in ACSL for specifying trigger to axioms. Another point to take into consideration : solvers are generally poor at reasoning with divisions. In the next major release of WP, you will find additional support for all these problems. Regards, L. Le 14 f?vr. 12 ? 14:03, <ds.verification at flecsim.com> <ds.verification at flecsim.com > a ?crit : > 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 > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss