Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject

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!&nbsp; 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--