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] E-ACSL v0.3
- Subject: [Frama-c-discuss] E-ACSL v0.3
- From: dmentre at linux-france.org (David MENTRE)
- Date: Tue, 24 Sep 2013 10:13:43 +0200
- In-reply-to: <524082A7.8080202@cea.fr>
- References: <524082A7.8080202@cea.fr>
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 """
- Follow-Ups:
- [Frama-c-discuss] RE : E-ACSL v0.3
- From: julien.signoles at cea.fr (SIGNOLES Julien)
- [Frama-c-discuss] RE : E-ACSL v0.3
- References:
- [Frama-c-discuss] E-ACSL v0.3
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] E-ACSL v0.3
- Prev by Date: [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
- Next by Date: [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
- Previous by thread: [Frama-c-discuss] E-ACSL v0.3
- Next by thread: [Frama-c-discuss] RE : E-ACSL v0.3
- Index(es):