--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2016 ---
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. - David -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160216/ec6febf3/attachment.html>