Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why axiom int32_extensionality (new in Nitrogen release) causes prover slow-down

Hi,

Le 18/11/2011 18:01, jochen a ?crit :
>
>
> Hello,
>
> while trying to adapt the document "ACSL By Example"
> (www.first.fraunhofer.de/fileadmin/FIRST/ACSL-by-Example.pdf) to version
> Nitrogen, we found that several procedures couldn't be verified under
> the new version, but could under the old one.
>
> A comparison generated proof obligations for some of those procedures
> revealed that the reason is the "Why axiom int32_extensionality", which
> could be rephrased in Acsl as something like the following:
>      \forall int x,y; (integer)x == (integer)y ==> x == y;

Yes, that's the idea, although your question is really specific to the 
Jessie plugin which has its own way to interpret == on int

> In some cases, the similar "Why axiom int8_extensionality" is also
> dangerous.
>
> When the former axiom is removed manually from the proof obligations
> file, our procedures pop_heap (p.101) and sort_heap (p.108) can be
> verified again, for example.

When I added this axiom to the Jessie model, I tried my own bench and 
did not notice such bad regression. Could you give me more details ? 
Does it happens with all provers or only for a particular one ?

> I'm aware that this is not a valid reason to omit that axiom again.
>
> On the other hand, I couldn't imagine a program where it is really
> needed. Seemingly, each program variable x is translated into (integer)x
> in the proof obligations, anyway.

That's not really true: a program variable x of type int is promoted to 
integer in contexts where it is required, such as a logic symbol which 
expect an integer.

> Hence there is no need to reason about
> int values, but only about integer values. Maybe, somebody can tell me a
> program where the axiom is in fact needed for verification?

A toy example of that would be

int x,y;

//@ axiomatic A { logic integer f(int n); }

/*@ ensures f(x) == f(y);
   @*/
void g(void) {
   x = 42; y = 42;
}

which, with the Jessie plugin, was not provable before the addition of 
the int32_extensionality axiom in the model. In such a case a simple fix 
would be to use the type integer for the parameter of f, but the problem 
occured in a more complex exemple where parameter of type int was really 
needed.

Again, this is specific to the Jessie way of computing verification 
conditions. I'd be happy to interact with you to understand better the 
problem.

- Claude



-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |