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



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>