diff options
| author | Peter Sewell | 2014-11-23 17:10:32 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-11-23 17:10:32 +0000 |
| commit | 840045c0048a0830f681473056fc13c8468819c7 (patch) | |
| tree | b11319c79cc1c534600bf3e5a44530798e219dd4 /src | |
| parent | 2fcc1972c06a7d6ff3b30c9285ed23c6bd7b0b09 (diff) | |
| parent | e9f592a544316166cc4c095cfd9702c96bccc75f (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/l2
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index e1ec6696..fdb55f5b 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -179,6 +179,10 @@ let rec extern_ifield_value v = match v with | Interp.V_vector fst inc bits -> bits_from_ibits bits | Interp.V_vector_sparse fst stop inc bits default -> extern_ifield_value (Interp_lib.fill_in_sparse v) + | Interp.V_lit (L_aux L_zero _) -> [Bitc_zero] + | Interp.V_lit (L_aux L_false _) -> [Bitc_zero] + | Interp.V_lit (L_aux L_one _) -> [Bitc_one] + | Interp.V_lit (L_aux L_true _) -> [Bitc_one] end let rec slice_reg_value v start stop = |