--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using structure object for precondition/postocndition



Hi everyone,
I'm Federico from university of Parma. I'm doing a Frama-C project and this
is my first approach with this program.
i send you my c program as attachment for more comprension of my problem.
i'm trying to write my first precondition and postcondition for the first
function in my program, Stack_init, i've need to write that the Stack
structure that i return is defined and an empty stack (for me an empty
stack is when the element of structure "size" is equal to 0), and my first
problem is here, i can't figure how i can access with ACSL into a structure
data. i've try with "ensure \result.size = 0" but not working.
i've also try to define the logical structure with "type Stack = struct
{real data[100]; real size}" but the program reply me with an "invalid
statment" because he don't recognize "{".
Thanks for the support

best regards
Federico Peruzzi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150903/b37cd93b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: simple_main.c
Type: text/x-csrc
Size: 2712 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150903/b37cd93b/attachment.c>