diff options
| author | Kathy Gray | 2014-11-23 17:07:10 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-23 17:07:10 +0000 |
| commit | e9f592a544316166cc4c095cfd9702c96bccc75f (patch) | |
| tree | 679e0dfaf0768121c117d41fed77b05124445bbf /src | |
| parent | d9d63b005c571b26cfcde8cdbfdf20f6aa39c563 (diff) | |
extern single bit and single bool to instruction_fields
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 f979b9d9..1ef14ad0 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -176,6 +176,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 = |