diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index d4792541..2997bc8b 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -344,7 +344,8 @@ let expand_bswap64 d s = assert false *) (* Handling of compiler-inlined builtins *) - +let last_system_register = 511l + let expand_builtin_inline name args res = let open Asmvliw in match name, args, res with (* Synchronization *) @@ -358,9 +359,15 @@ let expand_builtin_inline name args res = let open Asmvliw in | "__builtin_k1_stsud", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pstsud(res, a1, a2)) | "__builtin_k1_get", [BA_int(n)], BR(IR res) -> - emit (Pgetn(n, res)) + let cn = camlint_of_coqint n in + (if cn<0l || cn>last_system_register + then failwith (Printf.sprintf "__builtin_k1_get(n): n must be between 0 and %ld, was %ld" last_system_register cn) + else emit (Pgetn(n, res))) | "__builtin_k1_set", [BA_int(n); BA(IR src)], _ -> - emit (Psetn(n, src)) + let cn = camlint_of_coqint n in + (if cn<0l || cn>last_system_register + then failwith (Printf.sprintf "__builtin_k1_set(n, val): n must be between 0 and %ld, was %ld" last_system_register cn) + else emit (Psetn(n, src))) (* Byte swaps *) (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> |