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] One question about how to use Frama-c

  • Subject: [Frama-c-discuss] One question about how to use Frama-c
  • From: ziqing at udel.edu (Ziqing Luo)
  • Date: Thu, 30 Apr 2015 14:55:33 -0400
Hi Frama-c developers and users,

I'm trying to use Frama-c to prove some programs but I'm stuck at how to
use "assigns"  to express that all the cells of a 3-d array will be changed.


Take a simple example:

int a[2][2][2];

int foo() {

  a[1][1][1] = 0;

  return 0;

}

How should I add an annotation of "assigns" the whole array ?

I've tried using "assigns \forall integer i,j,k ;..." or just "assigns a",
but none of them works because "assigns" is expecting a left value.

Regards,

Ziqing Luo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150430/b26817ea/attachment.html>