--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on July 2015 ---
[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