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