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] Jessie - help proving adequate behavior on array computation in loops

  • Subject: [Frama-c-discuss] Jessie - help proving adequate behavior on array computation in loops
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 21 Oct 2014 12:53:59 +0200
  • In-reply-to: <1171957348.13519377.1413801825097.JavaMail.zimbra@inria.fr>
  • References: <1171957348.13519377.1413801825097.JavaMail.zimbra@inria.fr>
Hi,

I forward this mail to the Frama-C list, which is better because the 
problem is related to Frama-C

Your example exhibits a current issue in Frama-C with the interpretation 
of machine-dependent size of integer types. Shortly speaking, if you 
include in your example the standard sdtint.h header on a 64-bit 
machine, you will get

typedef int64_t long

The problem is that the default architecture of Frama-C is 32bits, hence 
long denote 32-bit sintegers, not 64-bits.

To fix your problem, you should run Frama-C with the option
-cpp-extra-args="-I$(frama-c -print-share-path)/libc"

The file I attach is fully proved using Frama-C/Jessie/Why3/Alt-Ergo, 
when running

frama-c -cpp-extra-args="-I$(frama-c -print-share-path)/libc" -jessie 
sum_arrays.c

Hope this helps,

- Claude

Le 20/10/2014 12:43, Jean-Karim Zinzindohoue a ?crit :
> Hello,
>
> I am looking into ways to verify C programs and there are a couple of
> things for which I would like to know if I could do better using
> Jessie/Frama-C/why3.
>
> Typically I would like to verify the following function :
>
> static void sum(int64_t *out, const int64_t *in) {
> int i;
>
> for(i = 0; i < 10; i++) {
> out[i] += in[i];
> }
> }
>
>
> But the best I could achieve was rewriting it that way :
>
>
> /*@
> requires \valid(out+(0..9)) && \valid(in+(0..9));
> requires \forall integer i ; 0 <= i < 10 ==> - INT64_MAX / 2 < out[i] &&
> out[i] < INT64_MAX / 2;
> requires \forall integer i ; 0 <= i < 10 ==> - INT64_MAX / 2 < in[i] &&
> in[i] < INT64_MAX / 2;
> requires \separated(out+(0..9), in+(0..9));
> ensures \forall integer i; 0 <= i < 10 ==> out[i] == \old(out[i]) + in[i];
> */
> static void sum(int64_t*out, const int64_t *in) {
>
>
> int i;
> int64_t tmp;
> int64_t cpy[10];
>
>
> //@ assert \forall integer j; 0 <= j < 10 ==> - INT64_MAX / 2 < out[j]
> && out[j] < INT64_MAX / 2;
> //@ assert \forall integer j; 0 <= j < 10 ==> - INT64_MAX / 2 < in[j] &&
> in[j] < INT64_MAX / 2;
>
>
>
> /*@
> loop invariant i >= 0 && i <= 10 &&
> \forall integer j; 0 <= j < i ==> cpy[j] == out[j] &&
> \forall integer j; 0 <= j < i ==> out[j] == \at(out[j],Pre) &&
> \forall integer j; 0 <= j < 10 ==> - INT64_MAX / 2 < out[j] && out[j] <
> INT64_MAX / 2;
> loop assigns cpy[0..9], i;
> loop variant 10 - i;
> */
> for (i = 0; i < 10; i++) {
> //@ assert i < 10 ==>- INT64_MAX / 2 < out[i] && out[i] < INT64_MAX / 2;
> cpy[i] = out[i];
> }
>
>
>
> i = 0;
> /*@
> loop invariant 0 <= i <= 10 &&
> \forall integer j; 0 <= j < i ==> out[j] == cpy[j] + in[j];
> loop variant 10 - i;
> */
> while (i < 10) {
> //@ assert - INT64_MAX < cpy[i] + in[i] < INT64_MAX;
> tmp = cpy[i] + in[i];
> out[i] = tmp;
> //@ assert out[i] == cpy[i] + in[i];
> i++;
> }
> }
>
>
> I did not manage to prove the code without having to copy the whole
> array first, which is not really acceptable performancewise.
>
> Just having a temporary variable in the loop like that :
>
> static void sum(int64_t *out, const int64_t *in) {
> int i; int64_t tmp;
>
> for(i = 0; i < 10; i++) {
>
> tmp = out[i] + in[i];
> out[i] = tmp;
> }
> }
>
> would be fine, but I did not manage to prove that either.
>
> Would there be a smart way of rewriting the code so that I could prove
> it's safety and behavioral correctness without having to copy the whole
> array "out" ?
>
> Also I am not able to use the ACSL "LoopEntry" and "LoopCurrent" labels
> with Jessie. Are they supported ?
>
>
> Best regards,
>
>
> Jean Karim
>
>
>
> _______________________________________________
> Why-discuss mailing list
> Why-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |

-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: sum_arrays.c
Type: text/x-csrc
Taille: 733 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141021/73c7b3d0/attachment.c>