Препроцессор Frama-C вставляет \ old в каждую ссылку указателя в разделе обеспечения

Question

Я использую версию Frama-C Silicon-20161101. Каждый раз, когда ссылка указывает значение указателя *x в предложении обеспечения, препроцессор вставляет *\old(x) без необходимости. Например

// File swap.c: 

/*@ requires \valid(a) && \valid(b); 
    @ ensures A: *a == \old(*b) ; 
    @ ensures B: *\at(\old(b),Post) == \old(*a) ; 
    @ assigns *a,*b ; 
    @*/ 
void swap(int *a,int *b) 
{ 
    int tmp = *a ; 
    *a = *b ; 
    *b = tmp ; 
    return ; 
} 

при обработке с frama-c swap.c -print выходами

/* Generated by Frama-C */ 
/*@ requires \valid(a) ∧ \valid(b); 
    ensures A: *\old(a) ≡ \old(*b); 
    ensures B: *\old(b) ≡ \old(*a); 
    assigns *a, *b; 
*/ 
void swap(int *a, int *b) 
{ 
    int tmp; 
    tmp = *a; 
    *a = *b; 
    *b = tmp; 
    return; 
} 

Интересно, что это все еще проверяется как правильная WP плагин! Я предполагаю, что это связано с тем, что *\old(a) - это значение столбца \old(a) (которое по-прежнему остается тем же самым указателем, поскольку оно не было изменено)? Это ошибка? Есть ли какое-нибудь быстрое исправление для пользователя?

Answer 1

В вашем вопросе есть две точки. Во-первых, *\old(a) не следует путать с \old(*a): в обоих случаях мы оцениваем указательa в Old состоянии, но в *\old(a), мы разыменовать его в текущем состоянии, в то время как в \old(*a), то разыменовать также сделано в состоянии Old.

Во-вторых, формальные параметры являются немного особенными: как указано в руководстве ACSL, в пост-состоянии функции они имеют то же значение, что и в предустановленном состоянии, даже если они были изменены функцией , например, в следующем:

/*@ 
    requires \valid(a + 0 .. 1); 
    ensures *a == \old(*a) + 1; 
    ensures a[1] == \old(a[1]) + 1; 
*/ 
void f(int *a) { 
    *a = *a + 1; 
    a++; 
    *a = *a + 1; 
} 

обоснованием здесь является то, что, так как C имеет вызова по значению семантики, внешний мир не может видеть любые внутренние изменения, внесенные в формальный (который выступает в качестве локальной переменной для этой цели). Другими словами, до тех пор, пока речь идет о контракте, значение, связанное с a в приведенном выше примере, является одним из фактических аргументов, переданных ему, независимо от того, что происходит при реализации функции. Обратите внимание, что в случае с указателем это, конечно, относится только к значению самого указателя, а не к значениям, хранящимся в блоке памяти, на который он указывает.

Чтобы сделать эту семантику явной, средство проверки типов обертывает все вхождения формального параметра в оговорку ensures внутри \old.

Вы также можете увидеть этот answer связанный, хотя и не совсем похожий вопрос.