Я только что установил из диспетчера пакетов Opam и пытаюсь научиться использовать анализ значений из учебника на веб-сайте frama-c. В настоящее время я не могу использовать файл builtin.c, это не в моей общей папке, и я не могу понять, как использовать -val-builtin (если это даже подходит).Значение Frama-C Builtins
Любые идеи о том, как это осуществить?
Я установил версию Frama-c 20151002.
Спасибо за помощь!
«Полуфабрикаты Frama-C», такие как Frama_C_interval, больше не нуждаются в реализации для анализа по значению. Следовательно, большая часть builtin.c была удалена, а остальная часть была добавлена в другие файлы. Все упоминания о builtin.c в руководстве могут быть проигнорированы, если вместо этого включен __fc_builtin.h. Аналогичным образом, builtin.h был заменен на __fc_builtin.h. (Но выдается предупреждение, чтобы информировать пользователя об этом факте.) Мы уточним руководства для Frama-C Aluminium, чтобы это разъяснить.
Какую версию следует использовать, я настоятельно рекомендую использовать магний (20151002). За эти годы было немало улучшений.
Ahh, я нашел __fc_builtin.h, но не был уверен, правильно ли это был файл. Благодаря!! – Fratink
Похоже, что пакет ubuntu имеет этот файл, но выпуск mainline 20151002 не работает. Просто начал использовать выпуск 2013 года в репозитории Ubuntu. – Fratink