Как отследить различия между исходным кодом C и предварительно обработанным кодом Frama-C?

Question

В frama-C, когда я загружаю исходный файл, он выполняет предварительную обработку и выполняет автоматическое исправление ошибок, например, "автоматическое приведение типов", как показано ниже (int является типизированным до float).

Теперь, как я могу увидеть все изменения, сделанные после предварительной обработки.

Есть ли какой-либо метод или файл журнала или предупреждающее сообщение, которое показывает все изменения, сделанные frama-c.! Это мой исходный код:

int main() {
int a, b;

printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, a/(float)b);

}

Это мой предварительно обработанный код frama-C:

extern int (/* missing proto */ printf)();
extern int (/* missing proto */ scanf)();
int main(void) {
int a;
int b;
int __retres;
printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, (float)a/(float)b);
__retres =0;
return (__retres);
}

Answer 1

API Frama-C предлагает определенное количество хуков, которые будут срабатывать для различий в случаях нормализации. Обратите внимание, что он не выполняет "автоматическое исправление ошибок". Выполненные преобразования не изменяют семантику программы.

Эти крючки расположены в cil/src/frontc/cabs2cil.mli Например, вы найдете там:

val typeForInsertedCast:
  (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) ref

typeForInsertedCast e t1 t2 вызывается, когда выражение e типа t1 должен быть косвенно преобразован в тип t2 (в условиях, описанных в разделе 6.3 стандарта C о неявных преобразованиях). Предоставляя здесь свою функцию через плагин, вы можете отслеживать все неявные преобразования, которые происходят в вашей программе.

Учебное пособие по написанию плагинов Frama-C доступно в руководстве пользователя (требуется знание OCaml).