[java] fix primitive types

Summary:
A java byte is not a short and a java character is not a C character. Fix those types by mapping them to what the spec ordains.

An extra advantage is that this establishes a bijection between java types and their project in the `sil` type system, so pretty printing in Java mode can actually be made to work.

Reviewed By: mityal

Differential Revision: D20330525

fbshipit-source-id: 00ac2294b
master
Nikos Gorogiannis 5 years ago committed by Facebook Github Bot
parent ddd09b83fd
commit 10afd021a1

@ -136,7 +136,7 @@ module Java = struct
| "boolean" -> | "boolean" ->
Typ.boolean Typ.boolean
| "char" -> | "char" ->
Typ.char Typ.java_char
| "long" -> | "long" ->
Typ.long Typ.long
| "float" -> | "float" ->

@ -273,9 +273,11 @@ let void = mk Tvoid
let void_star = mk (Tptr (void, Pk_pointer)) let void_star = mk (Tptr (void, Pk_pointer))
let java_byte = mk (Tint IShort) let java_char = mk (Tint IUShort)
let java_short = java_byte let java_byte = mk (Tint ISChar)
let java_short = mk (Tint IShort)
let boolean = mk (Tint IBool) let boolean = mk (Tint IBool)

@ -142,6 +142,8 @@ val mk_ptr : ?ptr_kind:ptr_kind -> t -> t
val void : t val void : t
(** void type *) (** void type *)
val java_char : t
val java_byte : t val java_byte : t
val java_short : t val java_short : t

@ -673,7 +673,7 @@ module Val = struct
else Taint.param_of_path path else Taint.param_of_path path
in in
match typ.Typ.desc with match typ.Typ.desc with
| Tint (IBool | IChar | ISChar | IUChar) -> | Tint (IBool | IChar | ISChar | IUChar | IUShort) ->
let v = itv_val ~non_int:is_java ~taint in let v = itv_val ~non_int:is_java ~taint in
if Language.curr_language_is Java then set_itv_updated_by_unknown v if Language.curr_language_is Java then set_itv_updated_by_unknown v
else set_itv_updated_by_addition v else set_itv_updated_by_addition v

@ -15,7 +15,7 @@ let translate_basic_type = function
| `Byte -> | `Byte ->
Typ.java_byte Typ.java_byte
| `Char -> | `Char ->
Typ.char Typ.java_char
| `Double -> | `Double ->
Typ.double Typ.double
| `Float -> | `Float ->

@ -15,15 +15,16 @@ module L = Logging
exception Type_tranlsation_error of string exception Type_tranlsation_error of string
(** https://docs.oracle.com/javase/tutorial/java/nutsandbolts/datatypes.html *)
let translate_basic_type = function let translate_basic_type = function
| `Int -> | `Int ->
Typ.int Typ.int
| `Bool -> | `Bool ->
Typ.boolean Typ.boolean
| `Byte -> | `Byte ->
Typ.char Typ.java_byte
| `Char -> | `Char ->
Typ.char Typ.java_char
| `Double -> | `Double ->
Typ.double Typ.double
| `Float -> | `Float ->

Loading…
Cancel
Save