summaryrefslogtreecommitdiff
path: root/x86/x86_extras_embed.lem
diff options
context:
space:
mode:
authorAlasdair2020-07-31 13:30:53 +0100
committerAlasdair2020-07-31 13:30:53 +0100
commitdd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch)
tree88d8d69e39b724902b280beaa8ce874e444f5dbc /x86/x86_extras_embed.lem
parent71db59830383b7db5316b5c99ccebe776fc837dc (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.lem24
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