Используя frama-c, мне нужно проанализировать алгоритм Евклида для вычисления наибольшего общего делителя между двумя числами с коэффициентами Безозута.Алгоритм принимает два положительных целых числа x и y в качестве входных данных и вычисляет два целых числа s и t, так что s · x + t · y = gcd (x, y)
Когда я запускаю код с использованием
frama-c-gui -val euclidEVA.c
для анализа, у меня возникает некоторое переполнение без знака& за пределами записи сгенерированных сигналов тревоги.
///*@
//requires ...
//*/
int main(int x, int y, int* pp, int* qp)
{
int s = 1, t = 0, u = 0, v = 1;
///*@
//loop invariant ...
//*/
while(y > 0)
{
int r = x % y;
int q = x / y;
x = y;
y = r;
int w = u;
u = s - u * q;
s = w;
w = v;
v = t - v * q;
t = w;
}
*pp = s; *qp = t;
return x;
}
- Какое предварительное условие я могу добавить для проверки доступа к памяти?
- Какой инвариант цикла можно добавить к пределу s и t ?
- Какой инвариант цикла можно добавить к границе u и v ?
- Какое предварительное условие я могу добавить для границ x и y в начале?
- Пожалуйста, сгенерируйте какие-либо комментарии к аварийным сигналам (переполнение со знаком и запись за пределы)?
снимок экрана сгенерированных аварийных сигналов
Спасибо.