Skip to content
Snippets Groups Projects
Commit 42a86155 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Add Variant annotation kind

parent 21615c0f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+ 2
− 0
View file @ 42a86155
...@@ -44,6 +44,7 @@ type annotation_kind = ...@@ -44,6 +44,7 @@ type annotation_kind =
| Precondition | Precondition
| Postcondition | Postcondition
| Invariant | Invariant
| Variant
| RTE | RTE
let kind_to_string loc k = let kind_to_string loc k =
...@@ -54,6 +55,7 @@ let kind_to_string loc k = ...@@ -54,6 +55,7 @@ let kind_to_string loc k =
| Precondition -> "Precondition" | Precondition -> "Precondition"
| Postcondition -> "Postcondition" | Postcondition -> "Postcondition"
| Invariant -> "Invariant" | Invariant -> "Invariant"
| Variant -> "Variant"
| RTE -> "RTE") | RTE -> "RTE")
let block stmt b = match b.bstmts with let block stmt b = match b.bstmts with
......
src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+ 1
− 0
View file @ 42a86155
...@@ -104,6 +104,7 @@ type annotation_kind = ...@@ -104,6 +104,7 @@ type annotation_kind =
| Precondition | Precondition
| Postcondition | Postcondition
| Invariant | Invariant
| Variant
| RTE | RTE
val runtime_check: val runtime_check:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment