--- layout: fc_discuss_archives title: Message 9 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



Hi,

> 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.
Moreover, let me recall that SMS solvers usually deals with infinite arrays, which is probably not what you want to deal with. So you might need to design a theory of finite arrays first.