--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on January 2012 ---
Hi everyone, I'm trying to verify the following code: void increment_ptr(unsigned int* array, unsigned int len, unsigned int* result) { *result = 0xffaabbcc; while(len > 0) { *result &= array[0]; array++; len--; } } using the Jessie plug-in/Frama-C Nitrogen. In order to get a proper loop invariant I decided to write it as an inductive predicate (as I always do). However, something that I really don't understand happens: - If I comment the line referent to array variable increment, the preservation of the loop invariant is (automatically) proved; - If I do not comment this line, I cannot prove the proof obligation related with the loop invariant preservation. For both cases, the corresponding line of the inductive predicate is commented. Please check the annotated code below. I was wondering if the problem is that Jessie does not support pointer arithmetic, however I found the following post http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000581.html in the Frama-C mailing list. I tried to find something related to this in the mailing list, but I didn't succeed. Does anybody can help me?! Best regards, B?rbara --- B?rbara Vieira HasLab / INESC TEC Dep. Inform?tica - Universidade do Minho ----------------------------------------------------------------------------------------------------------------------------------------------------------- /*@ inductive loop1{L1,L2}( unsigned int len1, unsigned int len2, unsigned int* result, unsigned int* array){ @ case base_case{L}: @ \forall unsigned int len; @ \forall unsigned int* result; @ \forall unsigned int* array; @ loop1{L,L}(len,len,result,array); @ case ind_case{L1,L2,L3}: @ \forall unsigned int len1,len2,len3; @ \forall unsigned int* result; @ \forall unsigned int* array; @ loop1{L1,L2}(len1,len2,result,array) ==> @ len3 == len2 -1 ==> @ \at(*result,L3) == (\at(*result,L2) & \at(array[0],L2)) ==> @ //\at(array,L3) == \at(array,L2) + 1 ==> //Line that corresponds to array++ @ loop1{L1,L3}(len1,len3,result,array); @ } @*/ /*@ requires len > 1 && \valid(array + (0..(len-1))) && \valid(result); @*/ void increment_ptr(unsigned int* array, unsigned int len, unsigned int* result) { *result = 0xffaabbcc; //@ assert \valid(array+0); //@ ghost unsigned int old_len = len; //@ ghost goto L1; //@ ghost L1: /*@ loop invariant 0<=len<=old_len; @ loop invariant loop1{L1,Here}(old_len,len,result,array); @ loop variant len; @*/ while(len > 0) { *result &= array[0]; //array++; len--; } } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120119/3fdbfae7/attachment.htm>