--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2017 ---
I want to prove the correctness of a simple function which adds two 3-by-3 matrices. Using wp plug-in, I can prove the assign clause but I can't prove the ensures clause (I use the real model for computing weakest preconditions). Did I forget a precondition, is it a known problem ? Regards, Arthur /*@ requires \valid(A[0]+(0..2)) && \valid(A[1]+(0..2)) && \valid(A[2]+(0..2)) && \valid(B[0]+(0..2)) && \valid(B[1]+(0..2)) && \valid(B[2]+(0..2)) && \valid(result[0]+(0..2)) && \valid(result[1]+(0..2)) && \valid(result[2]+(0..2)); requires \separated(A[0]+(0..2), A[1]+(0..2), A[2]+(0..2), B[0]+(0..2), B[1]+(0..2), B[2]+(0..2), result[0]+(0..2), result[1]+(0..2), result[2]+(0..2)); assigns result[0][0..2], result[1][0..2], result[2][0..2]; ensures \forall integer p, q; 0 <= p <= 2 && 0 <= q <=2 ==> result[p][q] == A[p][q] + B[p][q]; @*/ void matrix_addition(float A[3][3], float B[3][3], float result[3][3]){       /*@    loop assigns i, result[0][0..2], result[1][0..2], result[2][0..2];    loop invariant 0 <= i <= 3;    loop invariant \forall integer k; 0 <= k < i ==> result[k][0] == A[k][0] + B[k][0] && result[k][1] == A[k][1] + B[k][1] && result[k][2] == A[k][2] + B[k][2];    loop variant 2-i;    @*/    for (int i=0; i<3; i++){             /*@       loop assigns j, result[i][0..2];       loop invariant 0 <= j <= 3;       loop invariant \forall integer n; 0 <= n < j ==> result[i][n] == A[i][n] + B[i][n];       loop variant 2-j;       @*/       for (int j=0; j<3; j++){                   result[i][j] = A[i][j] + B[i][j];          //@ assert result[i][j] == A[i][j] + B[i][j];       }          }    } --   Arthur CLAVIÃRE Elève ingénieur SUPAERO - 2A ISAE SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace 10 avenue Edouard Belin - BP 54032 - 31055 TOULOUSE CEDEX 4 FRANCE - http://www.isae-supaero.fr Tel +33 5 61 33 80 80 - Fax (+33) 5 61 33 83 30 Plan d'accès/Access map -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170619/d6ca8c1c/attachment.html>