# 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] RE : E-ACSL v0.3

*Subject*: [Frama-c-discuss] RE : E-ACSL v0.3*From*: julien.signoles at cea.fr (SIGNOLES Julien)*Date*: Tue, 24 Sep 2013 19:54:38 +0000*In-reply-to*: <CAC3Lx=Z84xS_gadgAkVYhy_xbeDF_KV-P-2JSkrCeUFjnQpR-g@mail.gmail.com>*References*: <524082A7.8080202@cea.fr>, <CAC3Lx=Z84xS_gadgAkVYhy_xbeDF_KV-P-2JSkrCeUFjnQpR-g@mail.gmail.com>

Hello David, There is nothing strange about the logic behind E-ACSL notation. The example 2.5 is just totally wrong and you're fully right: it must be a disjunction || instead of a conjunction &&. It will be fixed in the next release of E-ACSL. By the way, this tset notation is not yet supported by E-ACSL v0.3. Please let me know if you need it in your examples. Thanks for this report, Julien ________________________________________ De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de David MENTRE [dmentre at linux-france.org] Date d'envoi : mardi 24 septembre 2013 10:13 ? : Frama-C public discussion Objet : Re: [Frama-c-discuss] E-ACSL v0.3 Hello Julien, 2013/9/23 Julien Signoles <Julien.Signoles at cea.fr>: > Enjoy this plug-in and do not hesitate to report your feedback. I just installed it but had no time to make extensive tests. At least it works as before on a simple example. :-) While skimming through the doc (e-acsl-implementation.pdf), I was surprised by the Example 2.5: """ Example 2.5 The set { x | integer x; 0 <= x <= 9 && 20 <= x <= 29 } denotes the set of all integers between 0 and 9 and between 20 and 29. """ Based on my comprehension of first order logic, I would have tell that this set is the empty set because an integer x cannot simultaneously be less than 9 AND bigger than 20. To denote the set of all integers between 0 and 9 and between 20 and 29, I would have written { x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }. What is the logic behind E-ACSL notation? Best regards, david PS: At least, B Method as the same understanding as me, the two following assertions are proved. ;-) """ MACHINE predicate_test CONSTANTS x1, x2 PROPERTIES (x1 = { yy | yy : INTEGER & 0 <= yy & yy <= 9 & 20 <= yy & yy <= 29 }) & (x2 = { yy | yy : INTEGER & ((0 <= yy & yy <= 9) or (20 <= yy & yy <= 29)) }) ASSERTIONS (x1 = {}) & (x2 = 0..9 \/ 20..29) END """ _______________________________________________ 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

**References**:**[Frama-c-discuss] E-ACSL v0.3***From:*Julien.Signoles at cea.fr (Julien Signoles)

**[Frama-c-discuss] E-ACSL v0.3***From:*dmentre at linux-france.org (David MENTRE)

- Prev by Date:
**[Frama-c-discuss] Assigns clause** - Next by Date:
**[Frama-c-discuss] Assigns clause** - Previous by thread:
**[Frama-c-discuss] E-ACSL v0.3** - Next by thread:
**[Frama-c-discuss] Assigns clause** - Index(es):