1
В frama-C, когда я загружаю исходный файл, он выполняет предварительную обработку и выполняет автоматическую коррекцию ошибок, такую как «автоматический тип», как показано ниже (int is typecasted to float).Как отслеживать различия между исходным кодом C и предварительно обработанным кодом Frama-C?
Теперь, как я могу увидеть все изменения, сделанные после предварительной обработки.
Есть ли способ или файл журнала или предупреждающее сообщение, которое показывает все изменения, сделанные рамкой-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 препроцессор кода: API
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);
}