Использование VST с GCC

Question

В руководстве Verified-C говорится

Какое бы наблюдаемое свойство программы на языке C вы ни доказали, используя логику проверяемой программы на языке C, это свойство фактически сохранится в программе на языке ассемблера, созданной компилятором C.

а потом

Логика программы проверена с точки зрения семантики CompCert C (...).

Что, если я использую другой компилятор (скажем, gcc — при условии, что сам gcc верен стандарту C)?

Предполагает ли логика (или clightgen) факты, которые не могут быть проверены каким-либо C-совместимым компилятором, не являющимся Compcert?

Редактировать:

Я провел небольшой эксперимент, скомпилировав его с помощью gcc и compcert.

      #include<stdio.h>
#include<limits.h>

int signed_overflow_expression(int x, int y) {
    return (x+y) > y;
}

int main(){
    printf("%i",signed_overflow_expression(INT_MAX,1));
}

gcc печатает 1, как описано здесь /questions/4489521/pochemu-kak-gcc-kompiliruet-neopredelennoe-povedenie-v-etom-teste-s-perepolneniem-so-znakom-chtobyi-on-rabotal-na-x86-no-ne-na-arm64/4489540#4489540.

Compcert печатает 0, потому что подписанное переполнение фактически определено поведением в Compcert C (см. §6.5 в руководстве Compcert https://compcert.org/man/manual005.html).

Однако VST требует, чтобы не было подписанных переполнений, поэтому я не могу доказать ничего, что было бы правильно для Compcert, а не для gcc. Это означает, что VST не совсем моделирует Compcert C, а является чем-то более близким к Standard C.

Кажется, это указывает на то, что я действительно могу использовать gcc, но мне интересно, есть ли другие ситуации, когда что-то может пойти не так.