diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml index d26f748a..0d09a20e 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml @@ -329,7 +329,7 @@ and get_field_memory_offset_at Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Skipped over field: " ^ (string_of_int offset)] - else if offset > (foff + sz) then + else if offset >= (foff + sz) then Ok None else let offset = offset - foff in @@ -369,7 +369,9 @@ and get_field_memory_offset_at Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Nonzero offset: " ^ (string_of_int offset) ^ " with unstructured field type: " - ^ (btype_to_string fldtype)]) + ^ (btype_to_string fldtype) + ^ " for field " + ^ finfo.bfname]) (resolve_type finfo.bftype)) (Ok None) finfos in (match optfield_r with | Error e -> Error e diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 2c316030..7bc460a0 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -832,6 +832,10 @@ object (self) (cv1: constant_value_variable_t) (cv2: constant_value_variable_t) = match (cv1, cv2) with + | (TypeCastValue _, TypeCastValue _) -> Stdlib.compare ix1 ix2 + | (TypeCastValue _, _) -> -1 + | (_, TypeCastValue _) -> 1 + | (FunctionReturnValue _, FunctionReturnValue _) -> Stdlib.compare ix1 ix2 | (FunctionReturnValue _, _) -> -1 | (_, FunctionReturnValue _) -> 1