Jak mam podejść do udowodnienia poprawności kodu, jak poniżej, który, aby uniknąć jakiejś nieefektywności, opiera się na modułowej arytmetyki?Dowody kodu, który opiera się na niepodpisanym całkowitym przepełnieniu?
#include <stdint.h>
uint32_t my_add(uint32_t a, uint32_t b) {
uint32_t r = a + b;
if (r < a)
return UINT32_MAX;
return r;
}
Mam eksperymentował z modelu „int” WP, ale, jeśli dobrze rozumiem, że wzór konfiguruje semantykę całkowitymi logicznych w OP, a nie formalne modele kod C. Na przykład, wtyczki WP i RTE wciąż wymagają i wstrzykują przepełnienie asercji PO dla niepodpisanego dodania powyżej podczas korzystania z modelu "int".
W takich przypadkach, czy mogę dodać adnotacje określające model logiczny dla instrukcji lub bloku podstawowego, więc mógłbym powiedzieć Frama-C, jak dany kompilator faktycznie interpretuje instrukcję? Jeśli tak, to czy mogę użyć innych technik weryfikacji w przypadku takich rzeczy, jak zdefiniowane, ale często wywołujące defekty zachowania, takie jak niepodpisane otoczenie, zachowania zdefiniowane przez kompilator, niestandardowe zachowania (wbudowane assy?) Itp., A następnie udowodnienie poprawności dla otaczający kod. Wyobrażam sobie coś podobnego do (ale silniejszego niż) "poprawki assert", używanej do informowania niektórych analizatorów statycznych, że pewne właściwości utrzymują się, gdy nie mogą samodzielnie wyprowadzić właściwości.
Pracuję z Frama-C Fluor-20130601, dla odniesienia, z alt-ergo 95.1.
One problem z twoim kodem: Niech 'a' będzie' UINT32_MIN' i niech 'b' będzie' -1'. Jak to się dzieje? (Nie mam tła z twoimi narzędziami/określonym kompilatorem) – BLaZuRE
@ BLaZuRE: b jest bez znaku, więc nie może być -1. –