From 8983f80895916c924ac0ba91f0e347555d554ff9 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 23 Feb 2022 09:21:43 +0000
Subject: [PATCH] Fixes demo example
---
_fc-plugins/acsl-importer.md | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/_fc-plugins/acsl-importer.md b/_fc-plugins/acsl-importer.md
index 0efbaf34..ddc922a5 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)));
--
GitLab