diff options
| author | Alasdair Armstrong | 2018-02-15 19:54:55 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-16 13:52:32 +0000 |
| commit | 00ca0aa4dce0abdcba574ce907e9a8a62d9d2255 (patch) | |
| tree | 31b1b0308d68210b483088346b471dfd468bb9d7 /aarch64/prelude.sail | |
| parent | 737ec26cf494affb346504c482e9b91127b68636 (diff) | |
Can now compile aarch64/duopod to C
Goes through the C compiler without any errors, but as we still don't
have all the requisite builtins it won't actually produce an
executable. There are still a few things that don't work properly,
such as vectors of non-bit types - but once those are fixed and the
Sail library is implemented fully it should work.
Diffstat (limited to 'aarch64/prelude.sail')
| -rw-r--r-- | aarch64/prelude.sail | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index ba5a3db7..55caddbb 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -105,7 +105,12 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} -val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +val UInt = { + ocaml: "uint", + lem: "uint", + interpreter: "uint", + c: "sail_uint" +} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) |