From ac798f9fb538e299cc9f1ede4a98430eb2d5e64e Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 4 Nov 2022 14:20:58 -0400
Subject: [PATCH] Added contract for `portDISABLE_INTERRUPTS` and dummy
 contracts for lock acquiring macros.

---
 .../verifast/proof/verifast_port_contracts.h  | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 verification/verifast/proof/verifast_port_contracts.h

diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h
new file mode 100644
index 000000000..57eb907e5
--- /dev/null
+++ b/verification/verifast/proof/verifast_port_contracts.h
@@ -0,0 +1,27 @@
+#ifndef VERIFAST_PORT_CONTRACTS_H
+#define VERIFAST_PORT_CONTRACTS_H
+
+
+/*@ 
+predicate interruptsOn_p(bool status);
+@*/
+
+#undef portDISABLE_INTERRUPTS
+#define portDISABLE_INTERRUPTS  VF__portDISABLE_INTERRUPTS
+void VF__portDISABLE_INTERRUPTS();
+//@ requires interruptsOn_p(_);
+//@ ensures interruptsOn_p(false);
+
+#undef portGET_TASK_LOCK
+#define portGET_TASK_LOCK  VF__portGET_TASK_LOCK
+void VF__portGET_TaskLock();
+//@ requires false;
+//@ ensures true;
+
+#undef portGET_ISR_LOCK
+#define portGET_ISR_LOCK  VF__portGET_ISR_LOCK
+void VF__portGET_ISR_LOCK();
+//@ requires false;
+//@ ensures true;
+
+#endif /* VERIFAST_PORT_CONTRACTS_H */
\ No newline at end of file