---
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
- Subject: [Frama-c-discuss] Pb with a simple pointer allocation
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Thu, 29 Apr 2010 14:43:08 +0200
- In-reply-to: <4BD8BC6A.7010307@univ-paris12.fr>
- References: <mailman.87.1272448828.12130.frama-c-discuss@lists.gforge.inria.fr> <4BD8BB3D.30201@univ-paris-est.fr> <4BD8BC6A.7010307@univ-paris12.fr>
> /*@ 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.