diff --git a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml
index 3987d4c0..867cb50d 100644
--- a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml
+++ b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml
@@ -87,6 +87,11 @@ let parse_cil_file ?(computeCFG=true) ?(removeUnused=true) (filename: string) =
            NL];
        exit 1
      end
+  | CHCommon.CHFailure p ->
+     begin
+       pr_debug [STR "Error when parsing "; STR filename; STR ": "; p; NL];
+       exit 1
+     end
   | e ->
      begin
        pr_debug [STR "Error when parsing (other exception): "; STR filename; NL];
diff --git a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml
index 89b7c8be..567b640a 100644
--- a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml
+++ b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml
@@ -891,6 +891,7 @@ let main () =
       let _ =
         if (List.length system_info#ifiles > 0) then
           pr_timing [STR "c header files parsed"] in
+      let _ = BCHBCTypeXml.register_ch_named_struct_types () in
       (* function annotations in userdata should be loaded after the header
          files are parsed, so types in the function annotations can be resolved.*)
       let _ = system_info#initialize_function_annotations in
diff --git a/CodeHawk/CHB/bchlib/bCHBCFiles.ml b/CodeHawk/CHB/bchlib/bCHBCFiles.ml
index 11122c28..1f683180 100644
--- a/CodeHawk/CHB/bchlib/bCHBCFiles.ml
+++ b/CodeHawk/CHB/bchlib/bCHBCFiles.ml
@@ -97,7 +97,8 @@ object (self)
   val vinfo_srcmap = H.create 3
   (* varinfo.ix -> (ix(filename), linenr, binloc, [ix(notes)]) *)
 
-  val mutable varinfo_vid_counter = 10000
+  val mutable varinfo_vid_counter = 100000
+  val mutable compinfo_ckey_counter = 100000
 
   method private get_varinfo_id =
     begin
@@ -105,6 +106,42 @@ object (self)
       varinfo_vid_counter
     end
 
+  method private get_compinfo_ckey =
+    begin
+      compinfo_ckey_counter <- compinfo_ckey_counter + 1;
+      compinfo_ckey_counter
+    end
+
+  method add_ch_named_struct_type (name: string) =
+    if H.mem gtypes name then
+      ()
+    else
+      let loc = {line = (-1); file = ""; byte = (-1)} in
+      let locix = bcd#index_location loc in
+      let structname = "_" ^ name ^ "_st" in
+      let ckey = self#get_compinfo_ckey in
+      let compinfo = {
+          bcstruct = true;
+          bcname = structname;
+          bckey = ckey;
+          bcfields = [];
+          bcattr = []
+        } in
+      let typeinfo = { btname = name; bttype = TComp (ckey, []) } in
+      begin
+        ignore (bcd#index_typeinfo typeinfo);
+        H.add gtypes name (bcd#index_typ typeinfo.bttype, locix);
+        H.replace
+          gcomptagdecls
+          (compinfo.bcname, compinfo.bckey)
+          (bcd#index_compinfo compinfo, locix);
+        log_result
+          ~tag:"add_ch_named_struct_type"
+          ~msg:name
+          __FILE__ __LINE__
+          [btype_to_string (typeinfo.bttype)]
+      end
+
   method add_bcfile (f: bcfile_t) =
     let i = bcd#index_location in
 
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml b/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml
index b9c134e7..28c12c41 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml
+++ b/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml
@@ -59,6 +59,14 @@ let raise_error (node: xml_element_int) (msg: pretty_t) =
   end
 
 
+let ch_named_struct_types = [
+    "ch_FILE"
+  ]
+
+let register_ch_named_struct_types () =
+  List.iter BCHBCFiles.bcfiles#add_ch_named_struct_type ch_named_struct_types
+
+
 (* Convert some standard type names as used in the legacy summaries to
    btype enumerations*)
 let get_standard_txt_type (t: string): btype_t option =
@@ -76,9 +84,12 @@ let get_standard_txt_type (t: string): btype_t option =
   | "Integer" -> Some (TInt (IInt, []))
   | "long" -> Some (TInt (ILong, []))
   | "LONG" -> Some (TInt (ILong, []))
+  | "off_t" -> Some (TInt (IULong, []))
   | "OLECHAR" -> Some (TInt (IWChar, []))
   | "size_t" -> Some (TInt (IUInt, []))
   | "SIZE_T" -> Some (TInt (IUInt, []))
+  | "ssize_t" -> Some (TInt (ILong, []))
+  | "time_t" -> Some (TInt (ILong, []))
   | "UINT" -> Some (TInt (IUInt, []))
   | "uint16_t" -> Some (TInt (IUShort, []))
   | "uint32_t" -> Some (TInt (IUInt, []))
@@ -88,8 +99,22 @@ let get_standard_txt_type (t: string): btype_t option =
   | "VOID" -> Some (TVoid ([]))
   | "wchar_t" -> Some (TInt (IWChar, []))
   | _ ->
-     let _ = chlog#add "legacy type name" (STR t) in
-     None
+     if List.mem t ch_named_struct_types then
+       begin
+         log_result
+           ~tag:"get_standard_txt_type:provided by typedef"
+           __FILE__ __LINE__
+           [t];
+         None
+       end
+     else
+       begin
+         log_result
+           ~tag:"get_standard_txt_type:legacy type not covered"
+           __FILE__ __LINE__
+           [t];
+         None
+       end
 
 
 let read_xml_summary_type (node: xml_element_int): btype_t =
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli b/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli
index a8ca0496..6353b16f 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli
+++ b/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli
@@ -45,3 +45,6 @@ val read_xml_returntype: xml_element_int -> btype_t
 val read_xml_summary_struct: xml_element_int -> bcompinfo_t
 
 val read_xml_type_transformer: xml_element_int -> type_transformer_t
+
+
+val register_ch_named_struct_types: unit -> unit
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
index 4072e79a..4906916a 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
@@ -518,6 +518,8 @@ class type bcfiles_int =
     (** [add_bcfile f] adds a parsed file [f] to the storage.*)
     method add_bcfile: bcfile_t -> unit
 
+    method add_ch_named_struct_type: string -> unit
+
     (** [add_fundef name type] adds an otherwise constructed function
         definition to the storage (i.e., not parsed).*)
     method add_fundef: ?attrs:b_attributes_t -> string -> btype_t -> unit
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
index 33661fce..25bb060f 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
@@ -375,4 +375,18 @@ let get_type_arg_mode
                | _ -> None) None predicates
       else
         mode in
+    let mode =
+      if Option.is_none mode then
+        List.fold_left (fun acc p ->
+            match acc with
+            | Some _ -> acc
+            | _ ->
+               match p with
+               | XXFreed (ArgValue param)
+                    when Option.is_some param.apar_index
+                         && (Option.get param.apar_index) = argindex ->
+                  Some ArgDeallocate
+               | _ -> None) None predicates
+      else
+        mode in
     mode
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index cb6f6670..f083f293 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3244,6 +3244,7 @@ type type_arg_mode_t =
   | ArgDerefReadWrite of int option
   | ArgDerefRead of int option
   | ArgDerefWrite of int option
+  | ArgDeallocate
   | ArgFunctionPointer
   | ArgScalarValue
 
@@ -3296,6 +3297,7 @@ type type_constant_t =
   | TyTStruct of int * string  (** bckey, bcname *)
   | TyTFloat of fkind_t
   | TyVoid   (** only to be used in the context of a void pointer *)
+  | TyNamed of string
   | TyTUnknown  (** top in type lattice *)
   | TyBottom  (** bottom in type lattice *)
 
diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml
index 7f5010e1..3e72aebb 100644
--- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml
+++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml
@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny B. Sipma
-   Copyright (c) 2021-2025 Aarno Labs LLC
+   Copyright (c) 2021-2026 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -146,6 +146,7 @@ let read_xml_sideeffect
       XXBlockWrite (get_type (arg 0), get_term (arg 1), get_term (arg 2))
     (* | "allocates-stack-memory" -> AllocatesStackMemory (get_term (arg 0)) *)
     | "modifies" -> XXModified (get_term (arg 0))
+    | "frees" -> XXFreed (get_term (arg 0))
     | "starts-thread" ->
       XXStartsThread (get_term (arg 0), List.map get_term (List.tl argNodes))
     | "invalidates" -> XXInvalidated (get_term (arg 0))
diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
index b72bf065..ca141550 100644
--- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
+++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyrigth (c) 2021-2025 Aarno Labs LLC
+   Copyrigth (c) 2021-2026 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -528,10 +528,11 @@ object
     | ArgDerefReadWrite _ -> "rw"
     | ArgDerefRead _ -> "r"
     | ArgDerefWrite _ -> "w"
+    | ArgDeallocate -> "d"
     | ArgFunctionPointer -> "fp"
     | ArgScalarValue -> "s"
 
-  method !tags = ["fp"; "r"; "rw"; "s"; "w"]
+  method !tags = ["d"; "fp"; "r"; "rw"; "s"; "w"]
 
 end
 
@@ -611,11 +612,12 @@ object
     | TyTStruct _ -> "ts"
     | TyTFloat _ -> "tf"
     | TyVoid -> "vp"
+    | TyNamed _ -> "n"
     | TyTUnknown -> "u"
     | TyBottom -> "b"
 
   method !tags = [
-      "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i";
+      "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i"; "n";
       "s"; "ti"; "tf"; "ts"; "u"; "vp"; "z"]
 
 end
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
index a95030b0..338c27fb 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
@@ -91,7 +91,8 @@ object (self)
       | ArgDerefReadWrite optsize
         | ArgDerefRead optsize
         | ArgDerefWrite optsize -> (tags, [index_opt optsize])
-      | ArgFunctionPointer
+      | ArgDeallocate
+        | ArgFunctionPointer
         | ArgScalarValue -> (tags, []) in
     type_arg_mode_table#add key
 
@@ -102,6 +103,7 @@ object (self)
     let a = a name args in
     let getsize () = if (a 0) = (-1) then None else Some (a 0) in
     match (t 0) with
+    | "d" -> ArgDeallocate
     | "fp" -> ArgFunctionPointer
     | "r" -> ArgDerefRead (getsize ())
     | "rw" -> ArgDerefReadWrite (getsize ())
@@ -215,6 +217,7 @@ object (self)
       | TyTStruct (key, name) -> (tags @ [name], [key])
       | TyTFloat k -> (tags @ [fkind_mfts#ts k], [])
       | TyVoid -> (tags, [])
+      | TyNamed s -> (tags @ [s], [])
       | TyBottom -> (tags, [])
       | TyTUnknown -> (tags, []) in
     type_constant_table#add key
@@ -236,6 +239,7 @@ object (self)
     | "ti" -> TyTInt (signedness_mfts#fs (t 1), a 0)
     | "tf" -> TyTFloat (fkind_mfts#fs (t 1))
     | "ts" -> TyTStruct (a 0, t 1)
+    | "n" -> TyNamed (t 1)
     | "vp" -> TyVoid
     | "b" -> TyBottom
     | "u" -> TyTUnknown
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
index 02da1b5e..06ec304b 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
@@ -660,6 +660,10 @@ object (self)
                             (List.map type_cap_label_to_string caps))])
             vars) evaluation in
     let result =
+      let promote (ty: btype_t): btype_t =
+        match ty with
+        | TInt _ -> BCHBCTypeUtil.promote_int ty
+        | _ -> ty in
       H.fold (fun k v a ->
           if v#isEmpty then
             if k = "return" then
@@ -683,7 +687,10 @@ object (self)
             match v#singleton with
             | Some ixty ->
                if k = "return" then
-                 begin returnresult := Some (bcd#get_typ ixty); a end
+                 begin
+                   returnresult := Some (promote (bcd#get_typ ixty));
+                   a
+                 end
                else
                  let optparamindex =
                    match k with
@@ -698,11 +705,14 @@ object (self)
                       if H.mem capresult k then
                         let caps = H.find capresult k in
                         List.flatten
-                          (List.map (convert_function_capabilities_to_attributes index) caps)
+                          (List.map
+                             (convert_function_capabilities_to_attributes index)
+                             caps)
                       else
                         []
                    | _ -> [] in
-                 (register_from_string k, Some (bcd#get_typ ixty), attrs) :: a
+                 let regty = promote (bcd#get_typ ixty) in
+                 (register_from_string k, Some regty, attrs) :: a
             | _ ->
                if k = "return" then
                  let _ =
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
index 940d87da..55246ec1 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
@@ -64,6 +64,9 @@ let _type_arg_mode_compare (m1: type_arg_mode_t) (m2: type_arg_mode_t): int =
      optvalue_compare i1 i2 Stdlib.compare
   | (ArgDerefWrite _, _) -> -1
   | (_, ArgDerefWrite _) -> 1
+  | (ArgDeallocate, ArgDeallocate) -> 0
+  | (ArgDeallocate, _) -> -1
+  | (_, ArgDeallocate) -> 1
   | (ArgFunctionPointer, ArgFunctionPointer) -> 0
   | (ArgFunctionPointer, _) -> -1
   | (_, ArgFunctionPointer) -> 1
@@ -139,6 +142,7 @@ let type_arg_mode_to_string (m: type_arg_mode_t) =
   | ArgDerefReadWrite i -> "rw" ^ (optsize_to_string i)
   | ArgDerefRead i -> "r" ^ (optsize_to_string i)
   | ArgDerefWrite i -> "w" ^ (optsize_to_string i)
+  | ArgDeallocate -> "d"
   | ArgFunctionPointer -> "fp"
   | ArgScalarValue -> "sv"
 
@@ -223,6 +227,7 @@ let type_constant_to_string (c: type_constant_t) =
   | TyTStruct (_, name) -> "t_struct_" ^ name
   | TyTFloat k -> float_type_to_string k
   | TyVoid -> "t_void"
+  | TyNamed name -> "t_named " ^ name
   | TyTUnknown -> "t_top"
   | TyBottom -> "t_bottom"
 
@@ -339,6 +344,9 @@ let join_tc (t1: type_constant_t) (t2: type_constant_t): type_constant_t =
       | _ -> TyTUnknown)
   | TyTInt _, _ -> t1
   | _, TyTInt _ -> t2
+  | TyNamed s1, TyNamed s2 when s1 = s2 -> t1
+  | TyNamed _, _ -> TyTUnknown
+  | _, TyNamed _ -> TyTUnknown
   | _, _ -> TyTInt (SignedNeutral, 8)
 
 
@@ -464,6 +472,7 @@ let convert_function_capabilities_to_attributes
     | ArgDerefReadWrite _ -> "read_write"
     | ArgDerefRead _ -> "read_only"
     | ArgDerefWrite _ -> "write_only"
+    | ArgDeallocate -> "deallocate"
     | ArgFunctionPointer -> "fp"
     | ArgScalarValue -> "sv" in
   let result = new CHUtils.IntCollections.set_t in
@@ -477,7 +486,7 @@ let convert_function_capabilities_to_attributes
                     AStr callsite;
                     AStr callee;
                     AInt argindex;
-                    ACons (type_arg_mode_to_attr_string mode, [])]) in
+                    AStr (type_arg_mode_to_attr_string mode)]) in
            result#add (bcd#index_attribute attr)
         | _ -> ()) caps in
   List.map bcd#get_attribute result#toList
@@ -575,6 +584,8 @@ let rec mk_btype_constraint
      end
   | Ok ty ->
      match ty with
+     | TNamed (s, _) ->
+        Some (TyGround (TyVariable tv, TyConstant (TyNamed s)))
      | TInt (ikind, _) ->
         let (signedness, size) = ikind_to_signedsize ikind in
         Some (TyGround
@@ -587,6 +598,9 @@ let rec mk_btype_constraint
      | TPtr (TVoid _, _) when use_voidptr ->
         let ptv = add_deref_capability tv in
         Some (TyGround (TyVariable ptv, TyConstant TyVoid))
+     | TPtr (TNamed (s, _), _) when use_voidptr ->
+        let ptv = add_deref_capability tv in
+        Some (TyGround (TyVariable ptv, TyConstant (TyNamed s)))
      | TPtr (TVoid _, _) -> None
      | TPtr (pty, _) ->
         let ptv = add_deref_capability tv in
@@ -665,6 +679,7 @@ let type_constant_to_btype (tc: type_constant_t) =
   | TyTStruct (key, _) -> get_compinfo_struct_type (bcfiles#get_compinfo key)
   | TyTFloat fkind -> TFloat (fkind, FScalar, [])
   | TyVoid -> t_void
+  | TyNamed s -> t_named s
   | TyBottom -> t_unknown
   | TyTUnknown -> t_unknown
 
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 11121daa..74ce3ea1 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20260324"
-  ~date:"2026-03-24"
+  ~version:"0.6.0_20260329"
+  ~date:"2026-03-29"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
index 6d90b833..ca68abb5 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
@@ -313,7 +313,13 @@ object (self)
                           end
                         else
                           log_type_constraint_rule_disabled __LINE__ rule tc
-                     | _ -> ())
+                     | _ ->
+                        log_diagnostics_result
+                          ~tag:"propagate_arg_to_param:no constraint"
+                          ~msg:(p2s floc#l#toPretty)
+                          __FILE__ __LINE__
+                          ["x: " ^ (x2s x);
+                           "btype: " ^ (btype_to_string argtype)])
                    ~error:(fun e ->
                      log_diagnostics_result
                        ~tag:mnem
@@ -330,6 +336,70 @@ object (self)
                 "call: " ^ (p2s floc#get_call_target#toPretty)];
            end in
 
+    let propagate_returnvar_to_function_return () =
+      let reg = register_of_arm_register AR0 in
+      let rvar = mk_function_typevar faddr in
+      let rvar = add_return_capability rvar in
+      let r0var = floc#env#mk_arm_register_variable AR0 in
+      let r0defs = get_variable_rdefs r0var in
+      let r0defs =
+        List.filter (fun d -> not (d#getBaseName = "init")) r0defs in
+      let rule = "POP-rdef-return" in
+      List.iter (fun r0def ->
+          let rettypeterm = mk_vty_term rvar in
+          let r0addr = r0def#getBaseName in
+          let ifloc =
+            get_i_floc floc (TR.tget_ok (string_to_doubleword r0addr)) in
+          let r0typevar = mk_reglhs_typevar reg faddr r0addr in
+          let r0var = floc#f#env#mk_register_variable reg in
+          let r0xvar = rewrite_floc_expr ifloc (XVar r0var) in
+          match r0xvar with
+          | XVar returnvar when floc#f#env#is_return_value returnvar ->
+             let callsite_r = floc#f#env#get_call_site returnvar in
+             TR.tfold_default
+               (fun callsite ->
+                 if floc#f#has_call_target callsite then
+                   let calltarget = floc#f#get_call_target callsite in
+                   let returntype = calltarget#get_returntype in
+                   let opttc = mk_btype_constraint rvar returntype in
+                   let rule = "POP-rdef-inv" in
+                   match opttc with
+                   | Some tc ->
+                      if fndata#is_typing_rule_enabled iaddr rule then
+                        begin
+                          log_type_constraint __LINE__ rule tc;
+                          store#add_constraint faddr iaddr rule tc
+                        end
+                      else
+                        log_type_constraint_rule_disabled __LINE__ rule tc
+                   | _ ->
+                      begin
+                        log_no_type_constraint __LINE__ rule returntype;
+                        ()
+                      end)
+               ()
+               callsite_r
+          | _ ->
+             let r0typeterm = mk_vty_term r0typevar in
+             begin
+               (if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then
+                  begin
+                    log_subtype_constraint __LINE__ rule r0typeterm rettypeterm;
+                    store#add_subtype_constraint
+                      faddr iaddr rule r0typeterm rettypeterm
+                  end
+                else
+                  log_subtype_rule_disabled __LINE__ rule r0typeterm rettypeterm);
+               (log_diagnostics_result
+                  ~tag:"Pop"
+                  ~msg:faddr
+                  __FILE__ __LINE__
+                  ["r0addr: " ^ r0addr;
+                   "r0xvar: " ^ (x2s r0xvar)])
+             end
+
+        ) r0defs in
+
     let getopt_stackaddress_r (x_r: xpr_t traceresult): int option =
       TR.tfold_default getopt_stackaddress None x_r in
 
@@ -1471,7 +1541,8 @@ object (self)
                   let r0typeterm = mk_vty_term r0typevar in
                   let rvartypeterm = mk_vty_term rvar in
                   let lhstypeterm = mk_vty_term typevar in
-                  if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then
+                  if fndata#is_typing_rule_enabled
+                       ~rdef:(Some r0addr) iaddr rule then
                     begin
                       log_subtype_constraint __LINE__ rule r0typeterm lhstypeterm;
                       log_subtype_constraint __LINE__ rule rvartypeterm lhstypeterm;
@@ -1484,89 +1555,8 @@ object (self)
                     log_subtype_rule_disabled __LINE__ rule r0typeterm lhstypeterm
                 ) r0defs);
 
-             (let rvar = mk_function_typevar faddr in
-              let rvar = add_return_capability rvar in
-              let r0var = floc#env#mk_arm_register_variable AR0 in
-              let r0defs = get_variable_rdefs r0var in
-              let r0defs =
-                List.filter (fun d -> not (d#getBaseName = "init")) r0defs in
-              let rule = "POP-rdef-return" in
-              List.iter (fun r0def ->
-                  let rettypeterm = mk_vty_term rvar in
-                  let r0addr = r0def#getBaseName in
-                  let ifloc =
-                    get_i_floc floc (TR.tget_ok (string_to_doubleword r0addr)) in
-                  let r0typevar = mk_reglhs_typevar reg faddr r0addr in
-                  let r0var = floc#f#env#mk_register_variable reg in
-                  let r0xvar = rewrite_floc_expr ifloc (XVar r0var) in
-                  match r0xvar with
-                  | XVar returnvar when floc#f#env#is_return_value returnvar ->
-                     let callsite_r = floc#f#env#get_call_site returnvar in
-                     TR.tfold_default
-                       (fun callsite ->
-                         if floc#f#has_call_target callsite then
-                           let calltarget = floc#f#get_call_target callsite in
-                           let returntype = calltarget#get_returntype in
-                           let opttc = mk_btype_constraint rvar returntype in
-                           let rule = "POP-rdef-inv" in
-                           match opttc with
-                           | Some tc ->
-                              if fndata#is_typing_rule_enabled iaddr rule then
-                                begin
-                                  log_type_constraint __LINE__ rule tc;
-                                  store#add_constraint faddr iaddr rule tc
-                                end
-                              else
-                                log_type_constraint_rule_disabled __LINE__ rule tc
-                           | _ ->
-                              begin
-                                log_no_type_constraint __LINE__ rule returntype;
-                                ()
-                              end)
-                       ()
-                       callsite_r
-                     (*
-                  | XVar param when floc#f#env#is_initial_register_value param ->
-                     let paramreg_r = floc#f#env#get_initial_register_value_register param in
-                     let pvar = mk_function_typevar faddr in
-                     TR.tfold
-                       ~ok:(fun paramreg ->
-                         let pvar =  add_freg_param_capability paramreg pvar in
-                         let ptypeterm = mk_vty_term pvar in
-                         let rtypeterm = mk_vty_term rvar in
-                         begin
-                           log_subtype_constraint __LINE__ rule ptypeterm rtypeterm;
-                           store#add_subtype_constraint
-                             faddr iaddr rule ptypeterm rtypeterm
-                         end)
-                       ~error:(fun e ->
-                         log_diagnostics_result
-                           ~tag:"Pop"
-                           ~msg:faddr
-                           __FILE__ __LINE__
-                           [String.concat "; " e])
-                       paramreg_r
-                      *)
-                  | _ ->
-                     let r0typeterm = mk_vty_term r0typevar in
-                       begin
-                         (if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then
-                            begin
-                              log_subtype_constraint __LINE__ rule r0typeterm rettypeterm;
-                              store#add_subtype_constraint
-                                faddr iaddr rule r0typeterm rettypeterm
-                            end
-                          else
-                            log_subtype_rule_disabled __LINE__ rule r0typeterm rettypeterm);
-                         (log_diagnostics_result
-                            ~tag:"Pop"
-                            ~msg:faddr
-                            __FILE__ __LINE__
-                            ["r0addr: " ^ r0addr;
-                             "r0xvar: " ^ (x2s r0xvar)])
-                       end
-
-                ) r0defs)
+             (if self#construct_signature then
+                propagate_returnvar_to_function_return ());
 
            end);
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml
index 69e1d002..97b8734c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml
@@ -16,7 +16,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="__fgetc_unlocked">
     <par loc="stack" name="stream" io="r" rep="hex" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
        <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml
index eafe11d7..504f34ea 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml
@@ -27,7 +27,7 @@
      <roles>
       <role rt="ioc:filesystem" rn="file" />
      </roles>
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
     </par>
    </api>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml b/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml
index 84b0514f..d55e577d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml
@@ -13,7 +13,7 @@
     </documentation>
     <api adj="0" cc="cdecl" name="clearerr">
       <par loc="stack" name="stream" nr="1">
-        <type><ptr>FILE</ptr></type>
+        <type><ptr>ch_FILE</ptr></type>
 	<pre><deref-read/></pre>
       </par>
       <returntype>void</returntype>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml b/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml
index 24b821f7..09b6722d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml
@@ -31,7 +31,7 @@
 	<pre><deref-read/></pre>
       </par>
       <par loc="stack" name="salt" nr="2">
-        <type><ptr>char></ptr></type>
+        <type><ptr>char</ptr></type>
 	<pre><deref-read/></pre>
       </par>
       <returntype><ptr>char</ptr></returntype>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml b/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml
index 49819697..35baaf51 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml
@@ -17,7 +17,7 @@
    <api adj="0" cc="cdecl" name="fclose">
     <returntype>int</returntype>
     <par loc="stack" name="stream" io="r" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
         <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
index 844d421c..74c8a2f4 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
@@ -33,7 +33,7 @@
      <type><ptr>char</ptr></type>
      <pre><deref-read-nt/></pre>
     </par>
-    <returntype><ptr>FILE</ptr></returntype>
+    <returntype><ptr>ch_FILE</ptr></returntype>
    </api>
    <semantics>
     <io-actions>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/feof.xml b/CodeHawk/CHB/bchsummaries/so_functions/feof.xml
index 7a5d3a85..39585e07 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/feof.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/feof.xml
@@ -16,7 +16,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="feof">
     <par loc="stack" name="stream" io="r" rep="hex" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <roles>
        <role rt="ioc:filesystem" rn="file"/>
      </roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml b/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml
index dd208f3c..ffce8f9e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml
@@ -16,7 +16,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="ferror">
     <par loc="stack" name="stream" io="r" rep="hex" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
        <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml b/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml
index e580721e..b61e06bc 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml
@@ -17,7 +17,7 @@
    <api adj="0" cc="cdecl" name="fflush">
      <returntype>int</returntype>
     <par loc="stack" name="stream" io="r" nr="1">
-      <type><ptr>FILE</ptr></type>
+      <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
       <roles>
          <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
index f83baf3f..90515f2b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
@@ -16,7 +16,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="fgetc">
     <par loc="stack" name="stream" io="r" rep="hex" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
        <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml
index 510b2f61..c35159db 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml
@@ -22,7 +22,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="fgetpos">
     <par loc="stack" io="r" name="stream" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
         <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
index 8ba63689..dab72e3d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
@@ -52,7 +52,7 @@
      <roles>
       <role rt="ioc:filesystem" rn="file" />
      </roles>
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
     </par>
    </api>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
index 99688644..f4496dae 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
@@ -17,7 +17,7 @@
    <api adj="0" cc="cdecl" name="fileno">
      <returntype>int</returntype>
     <par loc="stack" name="stream" nr="1">
-      <type><ptr>FILE</ptr></type>
+      <type><ptr>ch_FILE</ptr></type>
       <pre><deref-read/></pre>
       <roles>
 	<role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
index 7df95f74..1f1fe514 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
@@ -16,7 +16,7 @@
     </apidoc>
    </documentation>
    <api adj="0" cc="cdecl" name="fopen">
-    <returntype><ptr>FILE</ptr></returntype>
+    <returntype><ptr>ch_FILE</ptr></returntype>
     <par loc="stack" io="r" name="filename" rep="hex" nr="1">
       <type><ptr>char</ptr></type>
      <roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
index b217343c..ebabb7d2 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
@@ -16,7 +16,7 @@
     </apidoc>
    </documentation>
    <api adj="0" cc="cdecl" name="fopen64">
-    <returntype><ptr>FILE</ptr></returntype>
+    <returntype><ptr>ch_FILE</ptr></returntype>
     <par loc="stack" io="r" name="filename" rep="hex" nr="1">
       <type><ptr>char</ptr></type>
      <roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml
index 088cb79d..703551ba 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml
@@ -25,7 +25,7 @@
    <api adj="0" cc="cdecl" name="fprintf" varargs="yes">
      <returntype>int</returntype>
      <par loc="stack" name="stream" io="r" nr="1">
-       <type><ptr>FILE</ptr></type>
+       <type><ptr>ch_FILE</ptr></type>
        <pre><deref-read/></pre>
        <roles>
 	 <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
index d22dc527..01a708ec 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
@@ -27,7 +27,7 @@
      <roles>
       <role rt="ioc:filesystem" rn="file" />
      </roles>
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
     </par>
    </api>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
index f28dd3f0..84bac7de 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
@@ -33,7 +33,7 @@
      <roles>
       <role rt="ioc:filesystem" rn="file" />
      </roles>
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
     </par>
    </api>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
index c4c56721..4b8736d6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
@@ -41,7 +41,7 @@
       <pre><non-negative/></pre>
     </par>
     <par loc="stack" desc="file" io="r" name="stream" nr="4">
-      <type><ptr>FILE</ptr></type>
+      <type><ptr>ch_FILE</ptr></type>
       <roles>
         <role rt="ioc:filesystem" rn="file"/>
      </roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/free.xml b/CodeHawk/CHB/bchsummaries/so_functions/free.xml
index d2662a77..392eb255 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/free.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/free.xml
@@ -27,7 +27,16 @@
      </io-actions>
     <preconditions/>
     <postconditions/>
-    <sideeffects/>
+    <sideeffects>
+      <sideeffect>
+	<math>
+	  <apply>
+	    <frees/>
+	    <ci>ptr</ci>
+	  </apply>
+	</math>
+      </sideeffect>
+    </sideeffects>
    </semantics>
   </libfun>
   <copyright-notice>Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304</copyright-notice>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml b/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml
index fe799b87..87488ec0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml
@@ -25,7 +25,7 @@
     </documentation>
     <api adj="0" cc="cdecl" name="fscanf" varargs="yes">
       <par loc="stack" name="stream" nr="1">
-        <type><ptr>FILE</ptr></type>
+        <type><ptr>ch_FILE</ptr></type>
 	<pre><deref-read/></pre>
       </par>
       <par loc="stack" name="format" fmt="scan" nr="2">
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
index c0b09158..a56d8de0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
@@ -25,7 +25,7 @@
    <api adj="0" cc="cdecl" name="fseek">
     <returntype>int</returntype>
     <par loc="stack" io="r" name="stream" nr="1">
-       <type><ptr>FILE</ptr></type>
+       <type><ptr>ch_FILE</ptr></type>
      <roles>
         <role rt="ioc:filesystem" rn="file"/>
      </roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml b/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml
index 04ee20a9..2ae0d9d6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml
@@ -22,7 +22,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="fsetpos">
     <par loc="stack" io="r" name="stream" rep="hex" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <roles>
       <role rt="ioc:filesystem" rn="file" />
      </roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
index ac644668..45edd6a6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
@@ -17,7 +17,7 @@
    <api adj="0" cc="cdecl" name="ftell">
     <returntype>long</returntype>
     <par loc="stack" io="r" name="stream" nr="1">
-      <type><ptr>FILE</ptr></type>
+      <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
       <roles>
          <role rt="ioc:filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
index b4e945f7..e91a5032 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
@@ -36,7 +36,7 @@
       <type>size_t</type>
     </par>
     <par loc="stack" io="r" name="stream" nr="4">
-      <type><ptr>FILE</ptr></type>
+      <type><ptr>ch_FILE</ptr></type>
       <pre><deref-read/></pre>
       <roles>
          <role rt="filesystem" rn="file"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
index 6532c66e..f7fa9e0a 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
@@ -30,7 +30,7 @@
         <type>int</type>
       </par>
       <par loc="stack" name="stream" nr="3">
-        <type><ptr>FILE</ptr></type>
+        <type><ptr>ch_FILE</ptr></type>
 	<pre><deref-read/></pre>
       </par>
       <returntype>int</returntype>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
index eb8dfa6f..a19f0da8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
@@ -16,7 +16,7 @@
     </documentation>
     <api adj="0" cc="cdecl" name="pclose">
       <par loc="stack" name="stream" nr="1">
-        <type><ptr>FILE</ptr></type>
+        <type><ptr>ch_FILE</ptr></type>
 	<pre><deref-read/></pre>
       </par>
       <returntype>int</returntype>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
index 3055a19c..f3915bd9 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
@@ -29,7 +29,7 @@
         <type><ptr>char</ptr></type>
 	<pre><deref-read/></pre>
       </par>
-      <returntype><ptr>FILE</ptr></returntype>
+      <returntype><ptr>ch_FILE</ptr></returntype>
     </api>
     <semantics>
       <io-actions/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
index 3ef64db5..41bc5b60 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
@@ -34,7 +34,7 @@
     <api adj="0" cc="cdecl" name="realpath">
       <par loc="stack" name="file_name" nr="1">
 	<pre><deref-read-nt/></pre>
-        <type><ptr>char></ptr></type>
+        <type><ptr>char</ptr></type>
       </par>
       <par loc="stack" name="resolved_name" nr="2">
         <type><ptr>char</ptr></type>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
index 0832e333..1e739f68 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
@@ -13,7 +13,7 @@
    </documentation>
    <api adj="0" cc="cdecl" name="rewind">
     <par loc="stack" name="stream" nr="1">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <pre><deref-read/></pre>
      <roles>
        <role rt="ioc:filesystem" rn="stream"/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml b/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml
index 327c2568..36ad02d5 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml
@@ -25,7 +25,7 @@
      <type>int</type>
     </par>
     <par loc="stack" name="stream" io="r" rep="hex"  nr="2">
-     <type><ptr>FILE</ptr></type>
+     <type><ptr>ch_FILE</ptr></type>
      <roles>
        <role rt="ioc:filesystem" rn="file"/>
      </roles>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
index 05e622b6..ffef75bd 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
@@ -25,7 +25,7 @@
    <api adj="0" cc="cdecl" name="vfprintf">
      <returntype>int</returntype>
      <par loc="stack" desc="output stream" io="r" name="stream" nr="1">
-       <type><ptr>FILE</ptr></type>
+       <type><ptr>ch_FILE</ptr></type>
        <roles>
 	 <role rt="ioc:filesystem" rn="file"/>
        </roles>