Skip to content
Snippets Groups Projects
Commit 0e3a8691 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'baudin-master-patch-41201' into 'master'

Fixes demo example

See merge request !141
parents c8caf91a 8983f808
No related branches found
No related tags found
1 merge request!141Fixes demo example
Pipeline #42488 passed
......@@ -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)));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment