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]

[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.

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