Address review feedback

Author: dc-mak

frontend/model/cabs_to_ail_aux.lem

@@ -152,7 +152,6 @@ let rec mk_zeroInit_aux tagDefs (Ctype.Ctype _ ty) =
               error "[Cabs_to_ail.mk_zeroInit_aux] - internal ERROR: Union"
         end
     | Ctype.Byte ->
-        (* TODO: check *)
         A.ConstantInteger (A.IConstant 0 A.Octal Nothing)
   end
 let mk_zeroInit tagDefs ty =

frontend/model/core_aux.lem

@@ -48,7 +48,7 @@ let rec core_object_type_of_ctype (Ctype _ ty) =
    | Union tag_sym ->
        Just (OTy_union tag_sym)
    | Byte ->
-       (* TODO add an OTy_byte? *)
+       (* May need to revisit based on CN *)
        Just OTy_integer
   end
 

frontend/model/defacto_memory.lem

@@ -435,7 +435,7 @@ let rec mkUnspec (Ctype _ ty) =
         let ((memb_ident, (_, _, _, ty)), _) = Ctype_aux.get_unionDef tag_sym in
         MVunion tag_sym memb_ident (mkUnspec ty)
     | Byte ->
-        MVinteger Char (IV Prov_none IVunspecified)
+        MVinteger (Unsigned Ichar) (IV Prov_none IVunspecified)
   end
 
 

memory/concrete/impl_mem.ml

@@ -964,9 +964,8 @@ module Concrete : Memory = struct
           ( AbsByte.provs_of_bytes bs1
           , begin match extract_unspec bs1' with
               | Some cs ->
-                  let char_signed = (Ocaml_implementation.get ()).is_signed_ity Char  in
-                  MVinteger ( Char
-                            , mk_ival prov (int_of_bytes char_signed cs))
+                  (* C++ has std::byte typedef's to unsigned char, hence false *)
+                  MVinteger ( Char , mk_ival prov (int_of_bytes false cs))
               | None ->
                   MVunspecified cty
             end , bs2)

memory/vip/impl_mem.ml

@@ -452,8 +452,8 @@ match ty with
      let (bs1, bs2) = L.split_at (Common.sizeof cty) bs in
      ( begin match interp_bytes bs1 with
          | `SPECIFIED (prov_status, _, cs, _) ->
-             let char_signed = (Ocaml_implementation.get ()).is_signed_ity Char in
-             let n = int_of_bytes char_signed cs in
+              (* C++ has std::byte typedef's to unsigned char, hence false *)
+             let n = int_of_bytes false cs in
              MVinteger ( Char
                        , match prov_status with
                            | `NOPROV ->

ocaml_frontend/pprinters/pp_core_ctype.ml

@@ -87,7 +87,7 @@ let rec pp_ctype (Ctype (_, ty)) =
   | Union sym ->
       !^ "union" ^^^ pp_symbol sym (*!^(Pp_symbol.to_string sym)*)
   | Byte ->
-      !^ "cn_byte"
+      !^ "byte"
 
 
 (*