--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2009 ---
Thank you very much to all. An assert 0<>0 can't be automatically proved currently (With a timeout=400). Then I will probably try the second method : a coq model. Best regards, Nicolas. Claude March? a ?crit : > > Claude March? wrote: >> I don't understand why you are so pessimistic, Pascal. >> The answer is simple: just realize your axiomatization in Cuoq. Sorry: I >> meant in Coq. > > Another, probably quicker, possibility is first to try to prove > > //@ lemma l : 0=0; > > from your axiomatization. If it is proven, then yes surely you have to > investigate you axiomatization. A way to do it then is to remove parts > of it until you discovered the eaxt subset of axioms that can derive false. > > And if the lemme is not proven, then you might also try to prove > > //@ assert 0=0; > > just before return statement of the function that should not be proved > so quickly. And then proceed the same to remove some part of axiomatization. > > Hope this helps, > > - Claude > > _______________________________________________ > 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/20090407/a15d22f9/attachment.vcf