# 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.

# [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, 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

```