--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on October 2017 ---
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.