diff options
| -rwxr-xr-x | configure | 5 | ||||
| -rw-r--r-- | cparser/Machine.ml | 2 | ||||
| -rw-r--r-- | cparser/Machine.mli | 1 | ||||
| -rw-r--r-- | driver/Frontend.ml | 1 |
4 files changed, 7 insertions, 2 deletions
@@ -58,8 +58,9 @@ Supported targets: x86_64-cygwin (x86 64 bits, Cygwin environment under Windows) rv32-linux (RISC-V 32 bits, Linux) rv64-linux (RISC-V 64 bits, Linux) - kvx-mbr (Kalray KVX, bare runtime) - kvx-cos (Kalray KVX, ClusterOS) + kvx-mbr (Kalray KV3, bare runtime) + kvx-elf (Kalray KV3, ELF) + kvx-cos (Kalray KV3, ClusterOS) aarch64-linux (AArch64, i.e. ARMv8 in 64-bit mode, Linux) aarch64-macos (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 6c10715f..cc50be1e 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -287,6 +287,8 @@ let kvxmbr = { kvxbase with has_non_trapping_loads = true; } +let kvxelf = kvxmbr + let aarch64 = { i32lpll64 with name = "aarch64"; struct_passing_style = SP_ref_callee; (* Wrong *) diff --git a/cparser/Machine.mli b/cparser/Machine.mli index bdbec976..9e6063ba 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -91,6 +91,7 @@ val rv32 : t val rv64 : t val kvxmbr : t val kvxcos : t +val kvxelf : t val aarch64 : t val aarch64_apple : t diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 0d0ff26c..480932df 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -119,6 +119,7 @@ let init () = else Machine.rv32 | "kvx" -> if Configuration.os = "cos" then Machine.kvxcos else if Configuration.os = "mbr" then Machine.kvxmbr + else if Configuration.os = "elf" then Machine.kvxelf else (Printf.eprintf "Configuration OS = %s\n" Configuration.os; failwith "Wrong OS configuration for KVX") | "aarch64" -> if Configuration.abi = "apple" |