aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Machine.mli
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/Machine.mli')
-rw-r--r--cparser/Machine.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index f9d347b9..9e6063ba 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -18,6 +18,7 @@
type struct_passing_style =
| SP_ref_callee (* by reference, callee takes copy *)
| SP_ref_caller (* by reference, caller takes copy *)
+ | SP_value32_ref_callee (* by value if <= 32 bits, by ref_callee otherwise *)
| SP_split_args (* by value, as a sequence of ints *)
type struct_return_style =
@@ -60,6 +61,7 @@ type t = {
supports_unaligned_accesses: bool;
struct_passing_style: struct_passing_style;
struct_return_style: struct_return_style;
+ has_non_trapping_loads: bool;
}
(* The current configuration *)
@@ -87,6 +89,9 @@ val arm_littleendian : t
val arm_bigendian : t
val rv32 : t
val rv64 : t
+val kvxmbr : t
+val kvxcos : t
+val kvxelf : t
val aarch64 : t
val aarch64_apple : t