adding magic comment switches to CHERI

rems-project · Jul 28, 2023 · 82af1c1 · 82af1c1
1 parent 91355bf
commit 82af1c1
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git 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
@@ -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