--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pb with a simple pointer allocation



> /*@ lemma is_peraps_needed :
> @ \forall integer m, n; 0<m ==> 0<n ==> n<(m*n);
> @*/

Patrick Baudin pointed out to me at lunchbreak that this property is
false for m=n=1.