aboutsummaryrefslogtreecommitdiffstats
path: root/verilog/extractionMachdep.v
diff options
context:
space:
mode:
Diffstat (limited to 'verilog/extractionMachdep.v')
-rw-r--r--verilog/extractionMachdep.v20
1 files changed, 7 insertions, 13 deletions
diff --git a/verilog/extractionMachdep.v b/verilog/extractionMachdep.v
index 26a3f0a7..890735ba 100644
--- a/verilog/extractionMachdep.v
+++ b/verilog/extractionMachdep.v
@@ -14,21 +14,15 @@
(* *)
(* *********************************************************************)
-(* Additional extraction directives specific to the x86-64 port *)
+(* Additional extraction directives specific to the RISC-V port *)
-Require Archi SelectOp.
+Require Archi Asm.
(* Archi *)
-Extract Constant Archi.win64 =>
- "match Configuration.system with
- | ""cygwin"" when ptr64 -> true
- | _ -> false".
+Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ".
+Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *)
-(* SelectOp *)
-
-Extract Constant SelectOp.symbol_is_external =>
- "match Configuration.system with
- | ""macos"" -> C2C.atom_is_extern
- | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern
- | _ -> (fun _ -> false)".
+(* Asm *)
+Extract Constant Asm.low_half => "fun _ _ _ -> assert false".
+Extract Constant Asm.high_half => "fun _ _ _ -> assert false".