--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2013 ---
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>