frama-c-rppversion Documentation on ocaml.org
RPP plugin of Frama-C for writing and proving relational properties
RPP lets user write relational properties, that is properties that relate the state of the program during several execution of the same or different functions. It performs a code and specification transformation called self-composition to obtain a new C+ACSL program whose correctness (proved with WP) implies the validity of the relational property on the original code.
| Author | Lionel Blatter |
|---|---|
| License | LGPL-2.1-only |
| Published | |
| Homepage | https://frama-c.com/fc-plugins/rpp.html |
| Issue Tracker | https://git.frama-c.com/pub/frama-c/-/issues |
| Maintainer | virgile.prevosto@cea.fr |
| Dependencies | |
| Source [http] | https://github.com/lyonel2017/Frama-C-RPP/archive/refs/tags/v0.0.4.tar.gz md5=c1f95410aaa8839ae6b9c3e4dc13259a sha512=c999f46044866a492c8649cd68cb37b0f0ee90f1126ec5395df7ffcfbf6e0e52bc8c344d14c6f6fba17fca6c0ae1f27bf48fc4bc20ccfeaacf987c7376b7d203 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/frama-c-rpp/frama-c-rpp.0.0.4/opam |
No package is dependent
