From bbf63294f92e3bf25ce7c214b7249522c95ee17d Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Fri, 28 Jul 2023 17:15:52 -0700 Subject: [PATCH] maybe_revoke_pointer does not try to recover provenance --- coq/CheriMemory/CheriMemory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/CheriMemory/CheriMemory.v b/coq/CheriMemory/CheriMemory.v index c11ad2f97..7a6afb007 100644 --- a/coq/CheriMemory/CheriMemory.v +++ b/coq/CheriMemory/CheriMemory.v @@ -1531,7 +1531,7 @@ Module CheriMemory else let bs := fetch_bytes st.(bytemap) addr IMP.get.(sizeof_pointer) in '(_, mval, _) <- - serr2memM (abst DEFAULT_FUEL (find_overlapping_st st) st.(funptrmap) (fun _ => meta) addr + serr2memM (abst DEFAULT_FUEL (fun _ => NoAlloc) st.(funptrmap) (fun _ => meta) addr (CoqCtype.mk_ctype_pointer CoqCtype.no_qualifiers CoqCtype.void) bs) ;; match mval with