--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2013 ---
Hi Jens, > > int x = 0; > > > > /*@ requires y >= 0; > > @ ensures \result > x; > > @*/ > > int f(int y) { return y +1; } > > > in my opinion the function cannot be verified because the operation y+1 might overflow > in which case the result can become negative. Yes, you are right. But my main issue was that - if you use Coq for example - execpt the type of x, nothing is known about its value. I was looking for a minimal example. You have the same issue with an additional requires y < 10: -- Pierre-Lo?c Garoche Research Scientist @ ONERA pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu http://www.onera.fr/staff/pierre-loic-garoche/ -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 198 bytes Desc: Digital signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/2010d432/attachment.pgp>