From 11ab1a02b722a8f4a1c63b074c4c90a371a37225 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 28 Dec 2022 10:13:20 -0500
Subject: [PATCH] Deleted deprecated proof header.

---
 .../proof_setup/verifast_RP2040_axioms.h      | 19 -------------------
 .../tasks/vTaskSwitchContext/src/tasks.c      |  1 -
 2 files changed, 20 deletions(-)
 delete mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h
deleted file mode 100644
index b6dbda41f..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h
+++ /dev/null
@@ -1,19 +0,0 @@
-#ifndef VERIFAST_RP2040_AXIOMS_H
-#define VERIFAST_RP2040_AXIOMS_H
-
-#include "stdint.h"
-
-/*
- * The lemmas in this file axiomatize that the RP2040 architecture uses
- * 32bit pointers.
- */
-
-/*@
-// Axiomatizes that: 0 <= ptr <= 2^32 - 1
-lemma void ptr_range(void* ptr);
-requires true;
-ensures (void*) 0 <= ptr &*& ptr <= (void*) 4294967295;
-@*/
-
-
-#endif
\ No newline at end of file
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index 917960863..045f0c034 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -78,7 +78,6 @@
     #include "stack_predicates.h"
     #include "task_predicates.h"
     #include "ready_list_predicates.h"
-    #include "verifast_RP2040_axioms.h"
     #include "asm.h"
     #include "port_contracts.h"
     #include "lock_predicates.h"