Merge pull request #945 from hacspec/fstar-allow-unsafe

feat(engine/f*): allow unsafe code
hacspec · Oct 2, 2024 · bfcd974 · bfcd974
2 parents f8124b7 + cd59416
commit bfcd974
Show file tree

Hide file tree

Showing 7 changed files with 137 additions and 48 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -13,6 +13,7 @@ include
       include On.Construct_base
       include On.Quote
       include On.Dyn
+      include On.Unsafe
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -42,8 +43,7 @@ module SubtypeToInputLanguage
              and type for_index_loop = Features.Off.for_index_loop
              and type state_passing_loop = Features.Off.state_passing_loop
              and type match_guard = Features.Off.match_guard
-             and type trait_item_default = Features.Off.trait_item_default
-             and type unsafe = Features.Off.unsafe) =
+             and type trait_item_default = Features.Off.trait_item_default) =
 struct
   module FB = InputLanguage
 
@@ -59,6 +59,7 @@ struct
         include Features.SUBTYPE.On.Macro
         include Features.SUBTYPE.On.Quote
         include Features.SUBTYPE.On.Dyn
+        include Features.SUBTYPE.On.Unsafe
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -1685,8 +1686,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 
 module TransformToInputLanguage =
   [%functor_application
-  Phases.Reject.Unsafe(Features.Rust)
-  |> Phases.Reject.RawOrMutPointer
+    Phases.Reject.RawOrMutPointer(Features.Rust)
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait