Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Fri Nov 7 13:44:42 2008

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

Frama-C-discuss mailing list archives

[Frama-c-discuss] axiomatic permut redefined