--- layout: fc_discuss_archives title: Message 29 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



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