--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2014 ---
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>