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] axiomatic permut redefined
- Subject: [Frama-c-discuss] axiomatic permut redefined
- From: yannick.moy at gmail.com (Yannick Moy)
- Date: Fri Nov 7 13:44:42 2008
- In-reply-to: <295241148EBF4D9396BD767586C85B5A@AHARDPLACE>
- References: <295241148EBF4D9396BD767586C85B5A@AHARDPLACE>
Hi, First, thanks for being such a good bug-finder! I am answering both mails you sent today at once : 1) Regarding the problem of proving things with multiple labels on predicates, there should not be any problem with your code, btw there is indeed a missing label on refl axiom. We overlooked some problems with the interaction of our new axiomatic construct and multiple labels, that we are correcting now. After that, your code should check readily! 2) Regarding this message "Unexpected internal region in logic", it has to do with our handling of memory. This error can be raised easily on the following (incorrect, for us) axiomatic: /*@ axiomatic Bad { @ predicate pred(integer i); @ axiom bad: \forall int *p; pred(*p); @ } @*/ Indeed, this axiomatic makes predicate "pred" be dependent on some memory (pointed-to by int* pointers), but this memory is in no way related to the arguments of predicate "pred" at the state where it is called! Thus, we cannot find any value for this implicit argument to predicate "pred". This "limitation" should only be raised in these odd cases that we would like to avoid as much as possible. Your code does not fall in this case, it is a bug that we are going to look into. Sorry for these bad news for now! We come back soon with better ones ... Yannick On Fri, Nov 7, 2008 at 10:04 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Hi again, > > I have another problem I need help with. > > While I don't understand the axiomatic's well enough to do some serious > proving, I tried to implement a more functional approach of defining permut. > The idea is to count the occurrence of every element in each array and to > compare. Therefore I reused the NB_occ, given by Yannick: > > /*@ axiomatic NbOcc { > @ // nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j] > @ // (in a given memory state labelled L) > @ logic integer nb_occ{L}(int* t, integer i, integer j, > @ int e); > @ axiom nb_occ_empty{L}: > @ \forall int *t, e, integer i, j;i > j ==> nb_occ(t,i,j,e) == 0; > @ axiom nb_occ_true{L}: > @ \forall int *t, e, integer i, j; i <= j && t[j] == e ==> nb_occ(t,i,j,e) > == nb_occ(t,i,j-1,e) + 1; > @ axiom nb_occ_false{L}: > @ \forall int *t, e, integer i, j; i <= j && t[j] != e ==> nb_occ(t,i,j,e) > == nb_occ(t,i,j-1,e); > @ } > @*/ > > /*@ axiomatic IS_permutation { > logic integer is_permutation{L1,L2}(int* t1, int* t2, integer n); > axiom is_permutation_occ{L1,L2}: > \forall int *t1, *t2, n, integer i; i < n ==> > nb_occ{L1}(t1,0,n-1,\at(t1[i],L1)) == nb_occ{L2}(t2,0,n-1,\at(t2[i],L2)); > } > */ > > > /*@ > requires 0 <= length; > requires \valid_range(array1, 0, length-1); > ensures is_permutation{Old,Here}(array1, array1, length); > */ > void permute_test(int* array1, int length){} > > Doing this, I get following message: > > Uncaught exception: Failure("Unexpected internal region in logic") > > Unfortunately I have no clue what this means. > I would appreciate a hint whether the idea is doable and where are my > mistakes. > > Cheers > Christoph > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081107/076bd20f/attachment.html
- References:
- [Frama-c-discuss] axiomatic permut redefined
- From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
- [Frama-c-discuss] axiomatic permut redefined
- Prev by Date: [Frama-c-discuss] axiomatic permut redefined
- Next by Date: [Frama-c-discuss] Slicing: how to get rid of unused typedefs and other globals
- Previous by thread: [Frama-c-discuss] axiomatic permut redefined
- Next by thread: [Frama-c-discuss] Slicing: how to get rid of unused typedefs and other globals
- Index(es):