diff --git a/_fc-plugins/acsl-importer.md b/_fc-plugins/acsl-importer.md index 0efbaf349b4fae7a0b2c1572d2e18abff6222414..ddc922a578389413a2b2a56b39b3e5bfc1d77e3c 100644 --- a/_fc-plugins/acsl-importer.md +++ b/_fc-plugins/acsl-importer.md @@ -75,6 +75,13 @@ void job ( int *t , int A) { and a specification file: ``` +module demo : + axiomatic A { + type event = B | C(integer); + predicate P(integer x); + logic integer phi(event e); + } + function f: contract: ensures P(phi(C(\result)));