From 8060f89a5833b5af933bd451d71fea26a6b45ed3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Wed, 21 Apr 2021 18:01:57 +0200
Subject: [PATCH] forgotten file
---
include/arrow_spec.h | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
create mode 100644 include/arrow_spec.h
diff --git a/include/arrow_spec.h b/include/arrow_spec.h
new file mode 100644
index 00000000..7ac02a4b
--- /dev/null
+++ b/include/arrow_spec.h
@@ -0,0 +1,29 @@
+#ifndef ARROW_SPEC_H_
+#define ARROW_SPEC_H_
+
+/* ACSL arrow spec */
+//@ ghost struct _arrow_mem_ghost {struct _arrow_reg _reg;};
+/*@
+ predicate _arrow_valid(struct _arrow_mem *self) =
+ \valid(self);
+*/
+/*@
+ predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
+ mem_in._reg._first == 1;
+*/
+/*@
+ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
+ integer x, integer y,
+ struct _arrow_mem_ghost mem_out, _Bool out) =
+ (mem_in._reg._first ? (mem_out._reg._first == 0
+ && out == x)
+ : (mem_out._reg._first == mem_in._reg._first
+ && out == y));
+*/
+/*@
+ predicate _arrow_ghost(struct _arrow_mem_ghost mem,
+ struct _arrow_mem *self) =
+ mem._reg._first == self->_reg._first;
+*/
+
+#endif // ARROW_SPEC_H_
--
GitLab