Есть ли способ избавиться от обязательств доказательства alt-ergo, которые создает frama-c?
В настоящее время я играю с frama-c и хочу посмотреть, как frama-c кодирует различные обязательства по доказательству для передачи доказывающему (или помощнику по доказательству). В этом случае alt-ergo.
Мне было интересно, есть ли какой-либо конкретный способ "сбросить" ввод, переданный в alt-ergo (при условии, что alt-ergo вызывается из frama-c; то есть не взаимодействует)?
Я хотел бы увидеть, как обязательные свойства C-программ закодированы на "родном" языке ввода alt-ergo. Любая помощь будет принята с благодарностью.
1 ответ
Опция -wp-out <dir> позволяет выбрать <dir>как каталог, в который будут помещены сгенерированные файлы. Эти файлы отсортированы по подкаталогам в соответствии с используемой моделью памяти (typedпо умолчанию). Для Alt-Ergo вы должны найти файлы, заканчивающиеся на.ergo содержащие только обязательство по доказательству, и файлы, заканчивающиеся на _Alt-Ergo.mlw содержащий полный контекст обязательства доказательства (включая аксиомы, определяющие арифметические модели и модели памяти).
Однако обратите внимание, что в грядущем Frama-C 20.0 Calcium вводится использование API Why3 для связи с проверяющими, и в результате нативные выходы Alt-Ergo (и Coq) постепенно устаревают.