--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Define a Logic function returning an array





Is it possible to express a logic function returning an array in ACSL?

No it is not possible, unfortunately. The ACSL-By-Example <https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/ACSL-by-Example-12.1.0.pdf> document illustrate how to write logic predicates in ACSL dealing with C-arrays, but without manipulating « logic » arrays directly.

The current (up-to-date) version of “ACSL by Example” is available at

https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf

Regards

Jens Gerlach
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171028/a4eaf5aa/attachment.html>