--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2013 ---
Hello, 2013/11/5 Alessio Iotti <alle.iot at gmail.com>: > 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. As far as I know, neither WP nor Jessie do support these constructions: they are type-checked, but that's about all. Best regards, -- E tutto per oggi, a la prossima volta Virgile