diff options
Diffstat (limited to 'aarch64_small/armV8_extras_embed.lem')
| -rw-r--r-- | aarch64_small/armV8_extras_embed.lem | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem index 86570fc4..6b871344 100644 --- a/aarch64_small/armV8_extras_embed.lem +++ b/aarch64_small/armV8_extras_embed.lem @@ -51,9 +51,8 @@ let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST let DataSynchronizationBarrier_All () = barrier Barrier_DSB let InstructionSynchronizationBarrier () = barrier Barrier_ISB -val TMCommitEffect : unit -> M unit +val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e let TMCommitEffect () = barrier Barrier_TM_COMMIT -let duplicate_bits (Vector bits start direction,len) = - let bits' = repeat bits len in - Vector bits' start direction +val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type +let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |> |