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?

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