# 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] Question regarding frama-c/jessie

*Subject*: [Frama-c-discuss] Question regarding frama-c/jessie*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Mon, 01 Feb 2010 15:36:42 +0100*In-reply-to*: <4B62E1D5.5010500@adelard.com>*References*: <4B62E1D5.5010500@adelard.com>

Damien Karkinsky wrote: > Hello, > > We would like to prove properties on the set of all before/after states > for a given operation. For instance, suppose I have a C operation with > the following specification. > /*@ requires x >= 0; > @ ensures \result == x + 1; > */ > int increment(int x) { > return x + 1; > } > > I would like to prove a property like: > > /*@lemma (\forall int x, int y; (x >= 0 && y >= 0 ----or > rather some shorthand to satisfy the requires of operation "increment" > && y > x) > ==> > > Semantics_Of("increment")(y) > > Semantics_Of("increment")(x)) ---- i.e. operation > increment implements a monotonic function > */ > > > Could anyone tell me: > * whether such properties are expressible in ACSL > There is no direct support for that kind of property in ACSL. However, there are some tricks to acheive the same. The idea is the define an additional function which will call the former. For example: //@ requires x >=0 && y >= 0 && y > x; void check_increment_monotonicity(int x, int y) { int res_x = increment(x); int res_y = increment(y); //@ assert res_y > res_y; } I hope you get the idea... But beware, if the property you want depends on the global state, it will not work. Some methods based on this idea have been proposed, for example to prove properties of non-interference, e.g. private data can not be observable from public data. The general idea is, as above, to execute two independent copies of the code, but you have also to have two different copies of the heap in some sense. You could also look at the following paper which proposes methods to prove program equivalence using Frama-C: @inproceedings{almeida09fmics, author = {Almeida, Jos\'{e} Bacelar and Barbosa, Manuel and Sousa Pinto, Jorge and Vieira, B\'{a}rbara}, title = {Verifying Cryptographic Software Correctness with Respect to Reference Implementations}, booktitle = {Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'09)}, year = 2009, isbn = {978-3-642-04569-1}, pages = {37--52}, doi = {http://dx.doi.org/10.1007/978-3-642-04570-7_5}, publisher = SV } Hope this helps, - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |

- Prev by Date:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Next by Date:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Previous by thread:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Next by thread:
**[Frama-c-discuss] context sensitive points-to analysis** - Index(es):