Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CodeHawk/CH/chlib/cHNumerical.mli
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ val mkNumericalFromInt64 : int64 -> numerical_t
val mkNumericalFromString: string -> numerical_t


(** [mkNumericalPowerOf2 n] returns the numerical for 2^n] *)
(** [mkNumericalPowerOf2 n] returns the numerical for [2^n] *)
val mkNumericalPowerOf2: int -> numerical_t


Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CH/chutil/cHPrettyUtil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ val fixed_length_int_string: string -> int -> string
(** [string_suffix s n] returns the suffix of [s] that starts at the n'th
character of [s] (zero-based).

@raise Invalid_argument if [n] is larger than the length of [s]
raise Invalid_argument if [n] is larger than the length of [s]
*)
val string_suffix: string -> int -> string

Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CH/chutil/cHTraceResult.mli
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,12 @@ type 'a traceresult = ('a, string list) result


(** [tget_ok r] is [v] if [r] is [Ok v] and
@raise [Invalid_argument] otherwise.*)
raise [Invalid_argument] otherwise.*)
val tget_ok: 'a traceresult -> 'a


(** [tget_error r] is [e] if [r] is [Error e] and
@raise [Invalid_argument] otherwise.*)
raise [Invalid_argument] otherwise.*)
val tget_error: 'a traceresult -> string list


Expand Down
5 changes: 4 additions & 1 deletion CodeHawk/CH/xprlib/xsimplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -175,14 +175,17 @@ and reduce_neg (m: bool) (e1: xpr_t): (bool * xpr_t) =
| _ -> default ()


(* Note that for values other than zero the result depends on word size.*)
(* Note that, in general, for values other than zero the result depends on word
size. Here we assume that the word is at least 8 bits wide. *)
and reduce_bitwise_not (m: bool) (e1: xpr_t): (bool * xpr_t) =
let default () = (m, XOp (XBNot, [e1])) in
match e1 with
| XConst (IntConst num) when num#equal numerical_zero ->
(true, XConst (IntConst numerical_one#neg))
| XConst (IntConst num) when num#equal numerical_one ->
(true, XConst (IntConst (mkNumerical 2)#neg))
| XConst (IntConst n) when n#lt numerical_e8 ->
(true, XConst (IntConst (n#neg#sub numerical_one)))
| _ -> default ()


Expand Down
6 changes: 3 additions & 3 deletions CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -85,16 +85,16 @@ val t_charptr: btype_t
val ptr_deref: btype_t -> btype_t


(** {2 Array types)*)
(** {2 Array types} *)

val t_array: btype_t -> int -> btype_t


(** {2 Type definition}*)
(** {2 Type definition} *)

val t_named: string -> btype_t

(** {2 Composite types}*)
(** {2 Composite types} *)

val t_comp: ?name_space:string list -> string -> btype_t
val t_enum: ?name_space:string list -> string -> btype_t
Expand Down
8 changes: 4 additions & 4 deletions CodeHawk/CHB/bchlib/bCHBCTypes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -604,7 +604,7 @@ class type bcfiles_int =

(** [get_varinfo name] returns the varinfo with name [name].

@raise BCH_failure if no varinfo exists with name [name].*)
raise BCH_failure if no varinfo exists with name [name].*)
method get_varinfo: ?prefix:bool -> string -> bvarinfo_t

(** Returns all global varinfos (including functions) *)
Expand All @@ -622,7 +622,7 @@ class type bcfiles_int =
(** [get_typedef name] returns the (not necessarily fully expanded) type
definition associated with [name].

@raise BCH_failure if no typedef exists with name [name].
raise BCH_failure if no typedef exists with name [name].
*)
method get_typedef: string -> btype_t

Expand All @@ -640,7 +640,7 @@ class type bcfiles_int =
(** [get_compinfo key] returns the compinfo structure associated with
(CIL-assigned) key [key].

@raise BCH_failure if no compinfo definition or declaration exists
raise BCH_failure if no compinfo definition or declaration exists
with key [key].
*)
method get_compinfo: int -> bcompinfo_t
Expand All @@ -655,7 +655,7 @@ class type bcfiles_int =

(** [get_enuminfo name] returns the enuminfo structure with name [name].

@raise BCH_failure if no enuminfo definition or declaration exists with
raise BCH_failure if no enuminfo definition or declaration exists with
name [name]
*)
method get_enuminfo: string -> benuminfo_t
Expand Down
1 change: 1 addition & 0 deletions CodeHawk/CHB/bchlib/bCHBasicTypes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ open BCHLibTypes


exception BCH_failure of pretty_t
(** basic exception in all of CHB *)

(* raised in cases an internal inconsistency is encountered *)
exception Internal_error of string
Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHByteUtilities.mli
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ val rawdata_to_string:


(** [write_xml_raw_data elt s dw] writes byte string [s] to the xml element
[elt] in the form of sub elements with tag {aline} and attributes
{bytes} and {print} that contain 4 space-separated groups of 4 bytes in
[elt] in the form of sub elements with tag [aline] and attributes
[bytes] and [print] that contain 4 space-separated groups of 4 bytes in
hexadecimal and a print represenation of those 16 bytes, respectively.

This format is used in saving binary content of the sections to xml.*)
Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHCPURegisters.mli
Original file line number Diff line number Diff line change
Expand Up @@ -127,13 +127,13 @@ val full_registers: cpureg_t list
(** [mk_arm_sp_reg i] returns an ARM single-precision floating point register
(S<i>)

@raise BCH_failure if [i] is negative or i is greater than 31.*)
raise BCHBasicTypes.BCH_failure if [i] is negative or i is greater than 31.*)
val mk_arm_sp_reg: int -> arm_extension_register_t

(** [mk_arm_dp_reg i] returns an ARM double-precision floating point register
(D<i>)

@raise BCH_failure if [i] is negative or i is greater than 15.*)
raise BCH_failure if [i] is negative or i is greater than 15.*)
val mk_arm_dp_reg: int -> arm_extension_register_t


Expand Down
19 changes: 10 additions & 9 deletions CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ object (self)
| XPONotNull x ->
(match x with
| XConst (IntConst n) when n#gt numerical_zero ->
let n = n#modulo numerical_e32 in
Discharged
("non-null constant address: "
^ TR.tget_ok (numerical_to_hex_string n))
Expand All @@ -109,7 +110,7 @@ object (self)
| XPONullTerminated x ->
(match x with
| XConst (IntConst n) ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
if string_table#has_string dw then
Discharged ("constant string: " ^ (string_table#get_string dw))
else
Expand All @@ -119,7 +120,7 @@ object (self)
(match (ptr, size) with
| (XConst (IntConst n1), XOp ((Xf "ntpos"), [XConst (IntConst n2)]))
when n1#equal n2 ->
let dw = TR.tget_ok (numerical_to_doubleword n1) in
let dw = numerical_mod_to_doubleword n1 in
if string_table#has_string dw then
Discharged ("constant string: " ^ (string_table#get_string dw))
else
Expand All @@ -129,7 +130,7 @@ object (self)
(match (ptr, size) with
| (XConst (IntConst n1), XOp ((Xf "ntpos"), [XConst (IntConst n2)]))
when n1#equal n2 ->
let dw = TR.tget_ok (numerical_to_doubleword n1) in
let dw = numerical_mod_to_doubleword n1 in
if string_table#has_string dw then
Discharged ("constant string: " ^ (string_table#get_string dw))
else
Expand All @@ -138,7 +139,7 @@ object (self)
| XPOOutputFormatString x ->
(match x with
| XConst (IntConst n) ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
if string_table#has_string dw then
Discharged ("constant string: " ^ (string_table#get_string dw))
else
Expand Down Expand Up @@ -170,22 +171,22 @@ object (self)
let x = simplify_xpr x in
(match self#xprxt#xpr_to_bterm t_voidptr x with
| Some (NumConstant n) when n#gt numerical_zero ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
DelegatedGlobal (dw, XXNotNull (NumConstant n))
| Some t -> Delegated (XXNotNull t)
| _ -> Open)
| XPONullTerminated x ->
let x = simplify_xpr x in
(match self#xprxt#xpr_to_bterm t_voidptr x with
| Some (NumConstant n) when n#gt numerical_zero ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
DelegatedGlobal (dw, XXNullTerminated (NumConstant n))
| Some t -> Delegated (XXNullTerminated t)
| _ -> Open)
| XPOBlockWrite (ty, ptr, size) ->
(match self#xprxt#xpr_to_bterm t_voidptr ptr with
| Some (NumConstant n) when n#gt numerical_zero ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
(match self#xprxt#xpr_to_bterm t_int size with
| Some (NumConstant ns) ->
DelegatedGlobal
Expand All @@ -200,7 +201,7 @@ object (self)
| XPOBuffer (ty, ptr, size) ->
(match self#xprxt#xpr_to_bterm t_voidptr ptr with
| Some (NumConstant n) when n#gt numerical_zero ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
(match self#xprxt#xpr_to_bterm t_int size with
| Some (NumConstant ns) ->
DelegatedGlobal
Expand All @@ -215,7 +216,7 @@ object (self)
| XPOInitializedRange (ty, ptr, size) ->
(match self#xprxt#xpr_to_bterm t_voidptr ptr with
| Some (NumConstant n) when n#gt numerical_zero ->
let dw = TR.tget_ok (numerical_to_doubleword n) in
let dw = numerical_mod_to_doubleword n in
(match self#xprxt#xpr_to_bterm t_int size with
| Some (NumConstant ns) ->
DelegatedGlobal
Expand Down
8 changes: 4 additions & 4 deletions CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ val has_symbolic_address: string -> bool
(** [get_symbolic_address name] returns the address associated with name
[name].

@raise BCH_failure if no address exists with name [name].
raise BCH_failure if no address exists with name [name].
*)
val get_symbolic_address: string -> doubleword_int

Expand All @@ -96,20 +96,20 @@ val get_untyped_symbolic_address_names: unit -> string list
val update_symbolic_address_btype: string -> btype_t -> unit

(** [has_symbolic_address_name dw] returns true if the address [dw] is
associated with a name.]*)
associated with a name.*)
val has_symbolic_address_name: doubleword_int -> bool

(** [get_symbolic_address_name dw] returns the name associated with address
[dw].

@raise BCH_failure if no name is associated with address [dw]
raise BCH_failure if no name is associated with address [dw]
*)
val get_symbolic_address_name: doubleword_int -> string

(** [get_symbolic_address_type dw] returns the btype of the symbolic address
associated with address value [dw].

@raise BCH_failure if no symbolic address is associated with address [dw].
raise BCH_failure if no symbolic address is associated with address [dw].
*)
val get_symbolic_address_type: doubleword_int -> btype_t

Expand Down
6 changes: 3 additions & 3 deletions CodeHawk/CHB/bchlib/bCHDemangler.mli
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ open BCHLibTypes


(**
{[
{v
==============================================================================
Grammar
==============================================================================
Expand Down Expand Up @@ -164,13 +164,13 @@ open BCHLibTypes
U struct
V class
W enum
]}
v}

currently not supported yet:
- fields
- function pointers

*)
*)

val demangle: string -> string
val has_demangled_name: string -> bool
Expand Down
Loading