--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on June 2009 ---
Dear Eric and Jens, I will try to give a global response, but "jessie Masters" are still Yannick Moy and Claude March? O:-) The conversion Integer -> int is not costless for automatic provers. The "exact" option removes conversion predicates. It is then more efficient. However, is there any sense to prove a program without these conversions ? In my opinion, there is really 2 disjoint goals : * is my program correct without machine constraints ? (abstract Integers) --> exact option * are abstract values equals to concrete ones in previous PO ? --> if yes : just smile if not : same player play again, but without exact option. I don't know how to verify this second point. But I think that if a PO is valid with Integers and timeout without, then a manual proof can be tried. Regards, Nicolas. JENN Eric a ?crit : > As a followup to Jens' previous message (and to Nicolas answer to my > previous question), here is the translation of a message I sent directly > to Nicolas, in order to avoid cluttering the mailing list with my > (newbye) questions. Well, I think that it may be useful (not the > questions, but the answers to come...). > > "Actually, if I think that if I basically understand the differences > between those options (not their actual effect, but their meaning), I > miss some information to make an "operational choice": as I can't use > the strictiest model all the time, how shall I proceed? > > From what you write, I guess an approach could be to (i) try to verify > 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". > > This specific problem is part of a bigger set of issues: /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 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... > > Regards, > > Eric. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: nicolas_stouls.vcf Type: text/x-vcard Taille: 445 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090605/7f470c6f/attachment.vcf