aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2021-06-01 14:58:05 +0200
committerCyril SIX <cyril.six@kalray.eu>2021-06-01 14:58:05 +0200
commit75a2885f610e1d6e91df8e2386a4a4559b615bb9 (patch)
tree4456fa4a9876bc73d3d08b6dad1ad8f2f836578c /cparser
parent22504b61be43e5d4a97db621ce3c1785618bbaf0 (diff)
parentc44fc24eb6111c177d1d6fc973a366ebf646202b (diff)
downloadcompcert-kvx-75a2885f610e1d6e91df8e2386a4a4559b615bb9.tar.gz
compcert-kvx-75a2885f610e1d6e91df8e2386a4a4559b615bb9.zip
Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Machine.ml12
-rw-r--r--cparser/Machine.mli3
2 files changed, 12 insertions, 3 deletions
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index a0db245b..6c10715f 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -243,7 +243,7 @@ let rv64 =
struct_passing_style = SP_ref_callee; (* Wrong *)
struct_return_style = SR_ref } (* to check *)
-let kvx =
+let kvxbase =
{ name = "kvx";
char_signed = true;
wchar_signed = true;
@@ -276,7 +276,15 @@ let kvx =
supports_unaligned_accesses = true;
struct_passing_style = SP_value32_ref_callee;
struct_return_style = SR_int1to4;
- has_non_trapping_loads = true;
+ has_non_trapping_loads = false;
+}
+
+let kvxcos =
+ { kvxbase with has_non_trapping_loads = false;
+}
+
+let kvxmbr =
+ { kvxbase with has_non_trapping_loads = true;
}
let aarch64 =
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 11c73985..bdbec976 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -89,7 +89,8 @@ val arm_littleendian : t
val arm_bigendian : t
val rv32 : t
val rv64 : t
-val kvx : t
+val kvxmbr : t
+val kvxcos : t
val aarch64 : t
val aarch64_apple : t