--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using the \sum function



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>