--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL type invariants on array elements and fields



One practical issue is to build values of type T ; it is often the case where a value of type T must be created piecewise, with intermediate states actually breaking the invariant.
Similarly, strong invariants are hardly not usable in practice...
L.

> Le 5 mai 2015 ? 15:26, David R. Cok <dcok at grammatech.com> a ?crit :
> 
> Why does ACSL not require array elements and fields and memory locations of type T to satisfy type invariants for T - just global variables and parameters and, for strong invariants, local variables?
> 
> - David
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss