search

AllanBlanchard / tutoriel_wp

Frama-C and WP tutorial
Other
49 stars 17 forks source link

3.2.5.1 post conditions are not successfully proved (without pre conditions) #20

Closed alexioslyrakis closed 3 years ago

alexioslyrakis commented 3 years ago

In the exercise 3.2.5.1 it says "specify the post conditions until successfully proved (run without rte)". IMO, the tutorial solution would be:

/*@
    ensures *q * y + r == x;
    ensures *r < y;
*/
void div_rem(unsigned x, unsigned y, unsigned* q, unsigned* r) {
    *q = x / y;
    *r = x % y;
}

Unfortunately, I cannot get them proved without specifying pre-conditions. I would expect at least the latter one to be proved by Frama-C. The generated error is timeout (default is 10 sec).

AllanBlanchard commented 3 years ago

Argh, I forgot the total semantics of ACSL when I wrote this exercice.

It is indeed impossible to prove it without at least two properties in precondition :

Thank you, I'll fix that!

AllanBlanchard commented 3 years ago

(I just reopen the issue so that I do not forget to do it)

AllanBlanchard commented 3 years ago

OK, it is fixed, I do not know when I really did it O_o