--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2009 ---
all properties using the most constraining integer model, (ii) finalize the proof of properties that can't be verified with these constraints by relaxing the integer model and (iii) demonstrate (one way or another) that no overflow may occur for those variables considered "exact" rather than "bounded or modulo". <br> <br> This specific problem is part of a bigger set of issues: <i>how shall I write my pre, post, invariants to optimize the probability for all POs to be automatically discharged? How shall I handle a PO that lead to a timeout? (How do I analyze the problem?), Why are some POs discharged with one prover while another prover shows the"danger sign" ? What does it mean? etc. "</i><br> <br> I guess that I'll find an answer to all those questions while time passes and my close-to-null experience grows! Unfortunately, time is a bit missing over there... <br> <br> Regards,<br> <br> Eric.<br> </body> </html> --------------040503090609060209050008 Content-Type: text/x-vcard; charset=utf-8; name="eric.jenn.vcf" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="eric.jenn.vcf" begin:vcard fn:Eric JENN n:JENN;Eric org:Thales Avionics;AMS / MMAC adr;quoted-printable;dom:;;105, avenue du G=C3=A9n=C3=A9ral Eisenhower;Toulouse x-mozilla-html:TRUE version:2.1 end:vcard --------------040503090609060209050008--