--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on September 2015 ---
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>