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

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