--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on October 2008 ---
Hi there, (At first, please note that I'm currently running CVS version of Jessie & Why of october, 4) The following specification is verified by Automatic Theorem Provers on the small code just below: //@ requires \valid(p); assigns *p; ensures *p==4; void g(int*p){ while(1) *p=3; } In a way, [3==4] is validated because in the context of the related PO, one hypothesis is [true=false]. Does [true=false] hypothesis come with never ending loop? Am I missing something important here? Jessie's behavior seems to be very different than Caduceus' one on the matter of loops. And more generally speaking, what if end-users forget to annotate and validate loop variants to ensure loop termination? Nothing can tell them that they might prove anything as post-condition? Your opinion and explanations will be very welcome on these points? Cheers, Dillon Pariente