From 2fd6bcc2d730c6dacf209a40f87b1f5b7c9464f2 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 22 Nov 2022 07:14:21 -0500
Subject: [PATCH] Updated predicate `xLIST_ITEM` to jeep up with breaking VF
 change.

VeriFast now ensures that no uninitialised values are read. `x |-> _` is interpreted as "uninitialised", `x |-> ?v` is interpreted as "initialised".
---
 .../single_core_proofs/scp_list_predicates.h  | 47 ++++++++++++++-----
 1 file changed, 34 insertions(+), 13 deletions(-)

diff --git a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
index f91beb509..a839ee314 100644
--- a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
+++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
@@ -128,19 +128,40 @@
 	} List_t;
 #endif /* VERIFAST_SINGLE_CORE */
 
-/*@
-predicate xLIST_ITEM(
-	struct xLIST_ITEM *n,
-	TickType_t xItemValue,
-	struct xLIST_ITEM *pxNext,
-	struct xLIST_ITEM *pxPrevious,
-	struct xLIST *pxContainer;) =
-	n->xItemValue |-> xItemValue &*&
-	n->pxNext |-> pxNext &*&
-	n->pxPrevious |-> pxPrevious &*&
-	n->pvOwner |-> _ &*&
-	n->pxContainer |-> pxContainer;
-@*/
+#ifndef VERIFAST_SINGLE_CORE
+	/* Reason for deletion:
+	 * Breaking change in VeriFast. VeriFast now ensures that no uninitialised
+	 * values are read. `x |-> _` is interpreted as "uninitialised",
+	 * `x |-> ?v` is interpreted as "initialised".
+	 */
+	/*@
+	predicate xLIST_ITEM(
+		struct xLIST_ITEM *n,
+		TickType_t xItemValue,
+		struct xLIST_ITEM *pxNext,
+		struct xLIST_ITEM *pxPrevious,
+		struct xLIST *pxContainer;) =
+		n->xItemValue |-> xItemValue &*&
+		n->pxNext |-> pxNext &*&
+		n->pxPrevious |-> pxPrevious &*&
+		n->pvOwner |-> ?gOwner &*&
+		n->pxContainer |-> pxContainer;
+	@*/
+#else
+	/*@
+	predicate xLIST_ITEM(
+		struct xLIST_ITEM *n,
+		TickType_t xItemValue,
+		struct xLIST_ITEM *pxNext,
+		struct xLIST_ITEM *pxPrevious,
+		struct xLIST *pxContainer;) =
+		n->xItemValue |-> xItemValue &*&
+		n->pxNext |-> pxNext &*&
+		n->pxPrevious |-> pxPrevious &*&
+		n->pvOwner |-> _ &*&
+		n->pxContainer |-> pxContainer;
+	@*/
+#endif /* VERIFAST_SINGLE_CORE */
 
 /* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
 /*@