diff options
| author | Alasdair | 2020-07-31 13:30:53 +0100 |
|---|---|---|
| committer | Alasdair | 2020-07-31 13:30:53 +0100 |
| commit | dd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch) | |
| tree | 88d8d69e39b724902b280beaa8ce874e444f5dbc /x86/x86_extras_embed.lem | |
| parent | 71db59830383b7db5316b5c99ccebe776fc837dc (diff) | |
Remove old specs that have more up to date version
Move outdated things into old subdirectory
Diffstat (limited to 'x86/x86_extras_embed.lem')
| -rw-r--r-- | x86/x86_extras_embed.lem | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/x86/x86_extras_embed.lem b/x86/x86_extras_embed.lem deleted file mode 100644 index f5130995..00000000 --- a/x86/x86_extras_embed.lem +++ /dev/null @@ -1,24 +0,0 @@ -open import Pervasives -open import Pervasives_extra -open import Sail_impl_base -open import Sail_values -open import Prompt - -val rMEM : (vector bitU * integer) -> M (vector bitU) -val rMEM_locked : (vector bitU * integer) -> M (vector bitU) - -let rMEM (addr,size) = read_mem false Read_plain addr size -let rMEM_locked (addr,size) = read_mem false Read_X86_locked addr size - -val MEMea : (vector bitU * integer) -> M unit -val MEMea_locked : (vector bitU * integer) -> M unit - -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_locked (addr,size) = write_mem_ea Write_X86_locked addr size - -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () - -let X86_MFENCE () = barrier Barrier_x86_MFENCE |
