diff options
| author | Alasdair Armstrong | 2020-02-20 17:21:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2020-02-20 17:21:42 +0000 |
| commit | a04a740a3b564f2a9b09ca0a2366043eac3e8bc0 (patch) | |
| tree | 20bc2e3d495ecd317f7580378a58c906599675c5 /src/jib | |
| parent | 742eee392609a01b8565f4e64806ba0a14997844 (diff) | |
More list C codegen fixes for issue #59
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 7491b3e3..2b2234b5 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1481,6 +1481,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" | "undefined_bit", _ -> "UNDEFINED(fbits)" | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | "undefined_list", _ -> Printf.sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname in if fname = "reg_deref" then @@ -1890,6 +1891,12 @@ let codegen_list_equal id ctyp = ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) ^^ string "}" +let codegen_list_undefined id ctyp = + let open Printf in + ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) + ^^ ksprintf string " *rop = NULL;\n" + ^^ string "}" + let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in if IdSet.mem id !generated then @@ -1905,6 +1912,7 @@ let codegen_list ctx ctyp = ^^ codegen_cons id ctyp ^^ twice hardline ^^ codegen_pick id ctyp ^^ twice hardline ^^ codegen_list_equal id ctyp ^^ twice hardline + ^^ codegen_list_undefined id ctyp ^^ twice hardline end (* Generate functions for working with non-bit vectors of some specific type. *) |