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] scoping of 'axiomatic' declarations

Hello,

2016-01-17 2:06 GMT+01:00 David R. Cok <dcok at grammatech.com>:
> The acsl 1.9 document is unclear about the scoping of names declared in an
> axiomatic declaration.
>
> In the given example, are the declarations all essentially global and the
> name IntList just for convenience
> or is there some sort of scoping happening, like IntList::int_list or
> IntList::append_cons?

IntList is just here for convenience, and the declarations are global.
The Jessie plug-in takes advantage of the axioms enclosed in the
axiomatic to infer reads clauses for the declared symbols, so that it
is really important to group together declarations and their defining
axioms. Other than that (in particular if you use WP which relies
solely on user-provided reads clauses), axiomatics are just there to
help you structure syntactically your ACSL environment, and do not
play any semantic role.

Specification modules (section 2.6.11) would provide you namespaces,
but their are not implemented in Frama-C yet.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile