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 the \sum function

  • Subject: [Frama-c-discuss] Using the \sum function
  • From: alle.iot at gmail.com (Alessio Iotti)
  • Date: Tue, 5 Nov 2013 18:29:19 +0100
Dear All,

I attach a file containing a simple C program that (perhaps) computes the
average of an array of integers.
Frama-C can't prove the loop invariant and the ensures clause of the
contract, and in both there are uses of the built-in function \sum.
According to the paper "ACSL Version 1.7 - Implementation in
Fluorine-20130601", the functions \sum, \min, \max, \product and \numof are
experimental.
Then I copied the example at page 56 of the same paper, but, again, Frama-C
can't prove the clauses containing the \sum function.
So, my question is: I have to remove the \sum function from the annotations
or there is something else I can do to keep using that function?
Any help would be appreciated.
Kind regards,

   Alessio Iotti
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/c502967d/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: avg.c
Type: text/x-csrc
Size: 553 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131105/c502967d/attachment.c>