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] names of clauses, invariants, axioms

  • Subject: [Frama-c-discuss] names of clauses, invariants, axioms
  • From: cok at frontiernet.net (cok at frontiernet.net)
  • Date: Tue, 16 Feb 2016 12:40:35 +0000 (UTC)
  • References: <494530049.3914350.1455626436006.JavaMail.yahoo.ref@mail.yahoo.com>
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>