# 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

*Subject*: [Frama-c-discuss] Why axiom int32_extensionality (new in Nitrogen release) causes prover slow-down*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Tue, 22 Nov 2011 16:53:56 +0100*In-reply-to*: <4EC68F7A.5040001@first.fraunhofer.de>*References*: <4EC68F7A.5040001@first.fraunhofer.de>

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 |

**References**:**[Frama-c-discuss] Why axiom int32_extensionality (new in Nitrogen release) causes prover slow-down***From:*jochen.burghardt at first.fraunhofer.de (jochen)

- Prev by Date:
**[Frama-c-discuss] Why axiom int32_extensionality (new in Nitrogen release) causes prover slow-down** - Next by Date:
**[Frama-c-discuss] installing Nitrogen release on Mac** - Previous by thread:
**[Frama-c-discuss] Why axiom int32_extensionality (new in Nitrogen release) causes prover slow-down** - Next by thread:
**[Frama-c-discuss] installing Nitrogen release on Mac** - Index(es):