diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 10 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 6 |
2 files changed, 9 insertions, 7 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index b98c53c4..c13b7f3b 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -462,19 +462,19 @@ let analyze_primop' ctx id args typ = | "not_bits", [AV_cval (v, _)] -> AE_val (AV_cval (V_call (Bvnot, [v]), typ)) - | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ)) - | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ)) - | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ)) - | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ)) - | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ)) | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] -> diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 2066021e..e577e53a 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -193,8 +193,10 @@ let rec compile_aval l ctx = function let ctyp = cval_ctyp cval in let ctyp' = ctyp_of_typ ctx typ in if not (ctyp_equal ctyp ctyp') then - raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); - [], cval, [] + let gs = ngensym () in + [iinit ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs] + else + [], cval, [] | AV_id (id, typ) -> begin |