Я хотел бы сгенерировать все предварительные условия в основном исходные предпосылки в Frama-C

Я хотел бы сгенерировать все предварительные условия, созданные Frama-C, которые хранятся в таблице в соответствии с кодом calculus.ml. Мне в основном интересно получить начальный предикат, который преобразуется в логическую формулу и отправляется решателям. Это можно сделать? Пожалуйста, помогите мне распечатать начальный предикат, который отправляется решателям. Код, который я пытаюсь с приведен ниже:Я хотел бы сгенерировать все предварительные условия в основном исходные предпосылки в Frama-C

int main() 
{ 
    int x=42,y=40; 
    if(x<50) 
    { 
     x=x+2; y=x-y; 
    } 
    else 
    { 
     x=x-2; y=x-y; 
    } 
    //@ assert P: y>0; 
}

источник

2014-10-22 D.L.

Вы видели список опций WP с помощью '-wp-help'? Вы попробовали '-wp-print'? Если да, объясните, как он отличается от того, что вы пожелаете. – Anne

То, что я хочу, является начальным слабым предварительным условием в терминах логической формулы. Как для этого (x <=51^x-y> = 1) V (x> = 48^x-y> = 1) –

Это не WP вашего примера. WP является 'if (42 <50), тогда 42 + 2-40> 0 else 42-2-40> 0', который тривиально упрощается до True инструментом. Чтобы получить форму формулы, которую вы задаете, вам нужно преобразовать объявления x и y в формальные параметры функции. – Anne

Я думаю, что вы можете получить то, что вы хотите с помощью опции -wp-out dir, а затем посмотреть на сгенерированный .ergo файл в каталоге dir, но некоторые упрощения, возможно, уже было сделано. Я не думаю, что вы можете отключить эти внутренние упрощения.

источник

2014-10-23 06:42:24 Anne

Обязательства по доказательству не генерировались из-за qed. Теперь я получаю обязательства prof в каталоге, отключив qed с помощью -wp-no-simple. Спасибо за помощь. –

Я хотел бы сгенерировать все предварительные условия в основном исходные предпосылки в Frama-C

ответ

Смежные вопросы