Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Using structure object for precondition/postocndition
  • From: federico.peruzzi at studenti.unipr.it (FEDERICO PERUZZI)
  • Date: Thu, 3 Sep 2015 12:45:36 +0200
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>