c - frama-c wpの計算で反復ループを証明する方法は?

Question

配列セル内の各桁の表現に 2 つの long 整数を追加する (WP ループの不変条件を調べるための) テスト コードがあります。

int main(int argc, const char * argv[]) {

char a[32], b[32];//size can be very big
memset(a, 0, sizeof(a));
memset(b, 0, sizeof(b));
scanf("%s %s", a, b);
unsigned int size1 = strlen(a);
unsigned int size2 = strlen(b);
//code to reverse a string. currently proved 
reverse(a, size1);
reverse(b, size2);
for (unsigned int i = 0; i < size1; i++) a[i]-='0'; //move from chars to integers
for (unsigned int j = 0; j < size2; j++) b[j]-='0';
unsigned int maxsize = size1;
if (size2 > maxsize) maxsize = size2;
int over = 0;
//actual computation code

/*@
loop invariant maxsize == \max(size1, size2);
loop invariant bound: 0 <= k <= maxsize;
loop invariant ov: \forall integer i; 0 < i < k ==> \at(a[i], Here) == (\at(a[i], Pre) + b[i]+ Over((char *)a, (char *)b, i)) % 10;
loop assigns k, a[0..maxsize-1],over;
loop variant maxsize - k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
    char sum=a[k] + b[k] + over; 
    //over=overflow is for 9+9 = 18, result=8, over=1
    a[k] = sum % 10;
    over = sum / 10;
}
if (over != 0) a[maxsize++] = over;
//...
return 0;
}

最後のループの不変条件のみを指定したい。\at(a[i], LoopCurrent) を使用して ACSL コードをいくつか試しました。不明なステータスまたはタイムアウトを受け取りました。最後に、成功せずに公理的再帰ソリューションを終了しました。

これを確認するために他に何を試みるべきか、今のところわかりません。ヘルプ？

更新: 実際の計算用の関数を作成しました。改善された公理。まだタイムアウトステータスを取得しています。opam の Frama-C 最新リリースをデフォルト設定 (タイムアウト = 10、証明者 Alt-Ergo) で実行しました。

/*@
@predicate
Unchanged{K,L}(char* a, integer first, integer last) = \forall integer i; first <= i < last ==> \at(a[i],K) == \at(a[i],L);

axiomatic ReminderAxiomatic
{
logic integer Reminder {l} (integer x, integer y);
axiom ReminderEmpty: \forall integer x, integer y; x < y ==> Reminder(x, y) == x;
axiom ReminderNext: \forall integer x, integer y; x>=y ==> Reminder(x, y) == Reminder(x-y, y)+0; 
}

axiomatic DivAxiomatic
{
logic integer Div {l} (integer x, integer y);
axiom DivEmpty: \forall integer x, integer y; x < y ==> Div(x, y) == 0 ;
axiom DivNext: \forall integer x, integer y; x >= y ==> Div(x, y) == Div(x - y, y) + 1 ;
}

axiomatic OverAxiomatic
{
logic integer Over {L}(char *a, char * b, integer step) reads a[0..step-1], b[0..step-1];
axiom OverEmpty: \forall char *a, char * b, integer step; step <= 0 ==> Over(a, b, step) == 0;
axiom OverNext: \forall char *a, char * b, integer step; step > 0 && a[step-1]<10 && a[step-1]>=0 && b[step-1]<10 && b[step-1]>=0
==> Over(a, b, step) ==  Div((int) a[step-1]+(int)b[step-1]+(int)Over(a,b,step-1), 10);
}
*/
/*@
requires 0 <= maxsize < 10;
requires \valid (a+(0..maxsize-1));
requires \valid (b+(0..maxsize-1));
requires \valid (res+(0..maxsize));
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)a[i] < 10;
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)b[i] < 10;
*/
void summ(char *a, char *b, char *res, unsigned int maxsize) {

char over = 0;

/*@
loop invariant bound: 0 <= k <=maxsize;
loop invariant step: \forall integer i; 0 <= i < k ==> res[i] == (char) Reminder((int)a[i]+ (int)b[i]+ (int)Over((char *)a, (char *)b, i) , 10);
loop invariant unch: Unchanged{Here,LoopEntry}((char *)res, k, maxsize);
loop assigns k, over, res[0..maxsize-1];
loop variant maxsize-k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
 char sum = a[k] + b[k] + over;
 res[k] = sum % 10;
 over = sum / 10;
}

//
if (over != 0) res[maxsize++] = over;

}