diff options
Diffstat (limited to 'src/jib/jib_compile.ml')
| -rw-r--r-- | src/jib/jib_compile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 2f2e138e..b4837637 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -315,7 +315,8 @@ let rec compile_aval l ctx = function | V_lit (VL_bit Sail2_values.B1, _) -> [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] | _ -> - setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] [] CT_unit] @ cleanup + (* FIXME: Make this work in C *) + setup @ [iif (V_unary ("bit_to_bool", cval)) [icopy l (CL_id (gs, ctyp)) (V_op (V_id (gs, ctyp), "|", V_lit (mask i, ctyp)))] [] CT_unit] @ cleanup in [idecl ctyp gs; icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))] |