From 82af1c157efba969f0cf117aa9f133e414fcfb7c Mon Sep 17 00:00:00 2001 From: Kayvan Memarian Date: Fri, 28 Jul 2023 20:23:24 +0100 Subject: [PATCH] adding magic comment switches to CHERI --- coq/CheriMemory/CoqSwitches.v | 10 ++++++---- memory/cheri-coq/impl_mem.ml | 2 ++ 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/coq/CheriMemory/CoqSwitches.v b/coq/CheriMemory/CoqSwitches.v index c053e18bd..e7f583fda 100644 --- a/coq/CheriMemory/CoqSwitches.v +++ b/coq/CheriMemory/CoqSwitches.v @@ -19,10 +19,12 @@ Inductive cerb_switch : Set := | SW_strict_pointer_relationals : cerb_switch | SW_PNVI : SW_PNVI_values -> cerb_switch | SW_CHERI : cerb_switch -| SW_inner_arg_temps -| SW_permissive_printf -| SW_zero_initialised -| SW_revocation: SW_revocation_values -> cerb_switch. +| SW_inner_arg_temps : cerb_switch +| SW_permissive_printf : cerb_switch +| SW_zero_initialised : cerb_switch +| SW_revocation: SW_revocation_values -> cerb_switch +| SW_at_magic_comments : cerb_switch +| SW_warn_mismatched_magic_comments : cerb_switch. Lemma SW_pointer_arith_values_dec: forall x y:SW_pointer_arith_values, {x = y} + {x <> y}. Proof. decide equality. Qed. diff --git a/memory/cheri-coq/impl_mem.ml b/memory/cheri-coq/impl_mem.ml index 61a5381cd..a5c0fd25b 100644 --- a/memory/cheri-coq/impl_mem.ml +++ b/memory/cheri-coq/impl_mem.ml @@ -29,6 +29,8 @@ module CerbSwitchesProxy = struct | SW_zero_initialised -> SW_zero_initialised | SW_revocation `INSTANT -> SW_revocation INSTANT | SW_revocation `CORNUCOPIA -> SW_revocation CORNUCOPIA + | SW_at_magic_comments -> SW_at_magic_comments + | SW_warn_mismatched_magic_comments -> SW_warn_mismatched_magic_comments let toCoq_switches (cs: cerb_switch list): CoqSwitches.cerb_switches_t = let open ListSet in