aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Machine.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r--cparser/Machine.ml12
1 files changed, 10 insertions, 2 deletions
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 73b71ea0..4f5a93d2 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -242,7 +242,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;
@@ -275,7 +275,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 =