--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2016 ---
Hello David, 2016-02-16 13:40 GMT+01:00 cok at frontiernet.net <cok at frontiernet.net>: > Terms and predicates in ACSL can be given labels. In addition, some clauses, > such as invariants and axioms require an identifier. The ACSL 1.10 document, > at least, states that expression labels are purely for readability (and > perhaps error messages) and may not be used in other expressions (p. 17). > > Is the same true (in ACSL) for identifiers of invariants and axioms? > (Frama-C (Sodium) does not support invariants, and does not allow the > identifier of an axiom to be used as a predicate symbol). > > If not, this would be a useful feature - particularly for weak invariants. Axioms' names do not play any role in the current implementation. On the other hand, an invariant is also a predicate, with either 0 (for global invariants) or 1 (for type invariants) argument, and can be used as such. As you said, this is mainly useful for weak invariants, to assert that they hold at an arbitrary point beyond a function pre- or post-state. Best regards, -- E tutto per oggi, a la prossima volta Virgile