--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2016 ---
And just to be clear - you mean a predicate with zero arguments as in P(), not as P. - David On 2/16/2016 9:58 AM, Virgile Prevosto wrote: > 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,