From aaa53be077c82faff7ab1f7adff2232fa92a9246 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Tue, 13 Feb 2024 14:21:13 +0000 Subject: [PATCH] - Re-enabled 'test' caps as 'example' caps - Set git url in .opam to branch --- coq-cheri-capabilities.opam | 2 +- theories/Morello/Capabilities.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam index ed526ff..8cbce7a 100644 --- a/coq-cheri-capabilities.opam +++ b/coq-cheri-capabilities.opam @@ -30,4 +30,4 @@ build: [ "@doc" {with-doc} ] ] -dev-repo: "git+https://github.com/rems-project/coq-cheri-capabilities.git" +dev-repo: "git+https://github.com/rems-project/coq-cheri-capabilities.git#replacing_coq-sail_with_coq-sail-stdpp" diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index a3049a0..8367ed7 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -1124,7 +1124,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou End Capability. -(* Module TestCaps. +Module ExampleCaps. (* c1 corresponds to https://www.morello-project.org/capinfo?c=1900000007f1cff1500000000ffffff15 *) Definition c1:Capability.t := Capability.of_Z 0x1900000007f1cff1500000000ffffff15. @@ -1140,4 +1140,4 @@ End Capability. Definition c3_bytes := ["208"%char;"230"%char;"255"%char;"255"%char;"000"%char;"000"%char;"000"%char; "042"%char;"208"%char;"230"%char;"212"%char;"102"%char;"000"%char;"000"%char;"000"%char;"220"%char]. -End TestCaps. *) +End ExampleCaps.