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] Prove the reverse of a char*, ensure problems

Hi and thanks for answering. I didn't install any particular plugin, I just did "sudo apt-get installa frama-c", nothing more.

This is the full code:

(Note that the three "ensures" are just my trials. I would like just one to be proved and understand why the others' not)



/*@
 requires \valid(a);
 requires \valid(b);

 assigns(*a);
 assigns(*b);

 ensures *a == \old(*b);
 ensures *b == \old(*a);
*/
void swap(char *a, char *b)
{
 const char tmp = *a;
 *a = *b;
 *b = tmp;
}

/*@
 logic char* get_reverse{L}(char *s, integer n) =
  n < 2 ?
   s :
   get_reverse(s+1, n-2);
*/

/*@
 predicate reversed_recursive{L1,L2}(char *a, char *b, integer n) =
  n <= 1 ?
  \at(*a, L1) == \at(*b, L2) :
  (\at(a[0], L1) == \at(b[n-1], L2)) && reversed_recursive{L1,L2}(\at(a+1, L1), \at(b, L2), n-1);
*/

/*@
 predicate reversed_iterative{L1,L2}(char* a, char* b, unsigned n) =
  \forall unsigned i;
  0 <= i < n ==> \at(a[i], L1) == \at(b[n-i-1], L2);
*/

/*@
 requires n>= 0;
 requires \valid(s+(0 .. n-1));

 assigns s[0..(n-1)];

 ensures reversed_recursive{Pre,Post}(\at(s, Pre), \at(s, Post), n);
 
 ensures \forall unsigned i;
  0 <= i < n ==> \at(s[i], Pre) == \at(s[n-i-1], Post);

 ensures \at(s, Pre) == get_reverse{Post}(\at(s, Post), n);

*/
void reverse(char *s, unsigned n)
{
    if (n < 2)
  return;
 
 swap(s, s + (n - 1));
    reverse(s + 1, n - 2);
}    




Thanks you very much for your patience.
Francesco


----------------------------------------
> Date: Tue, 21 Jul 2015 11:11:34 +0200
> From: Claude.Marche at inria.fr
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Prove the reverse of a char*, ensure problems
>
>
> Hello,
>
> Which plugin are you using for proving your code?
> Could you provide the full input file instead of a few pieces?
>
> - Claude
>
> --
> Claude Marché | tel: +33 1 69 15 66 08
> INRIA Saclay - ÃŽle-de-France |
> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex |
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss