diff options
| author | Brian Campbell | 2018-08-07 11:02:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-07 11:14:20 +0100 |
| commit | f9282ab5dec29d7ec99d473d013d32b41a0b8dbc (patch) | |
| tree | 97908cf43a4eb858a6be57e7b370eba503b6cf03 /lib | |
| parent | 6538b63c944e32692447423829f8f4e91428b473 (diff) | |
Improve cast introduction for Lem
Handles mutable variables and conditionals (there are still some corner
cases that don't appear in Aarch64 to do).
The pretty printer is now back to preferring to use concrete types, but
has a special case for casts to print more general types.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/mono_rewrites.sail | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index aa8d05cd..9e837e10 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v) /* This is generated internally to deal with case splits which reveal the size of a bitvector */ -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure /* Definitions for the rewrites */ |