CHC: change in MemoryAddress representation

Author: sipma

CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli

@@ -130,6 +130,7 @@ object
   method mk_stack_address_value: varinfo -> offset -> typ -> variable_t
   method mk_memory_address_value: int -> offset -> variable_t
   method mk_string_address: string -> offset -> typ -> variable_t
+  method mk_initial_value: variable_t -> typ -> variable_type_t -> variable_t
 
   method mk_function_return_value:
            location
@@ -246,6 +247,7 @@ object
   method get_indicator: variable_t -> int  (* augmentation variable *)
 
   method get_initial_parameter_vinfo: variable_t -> varinfo * offset
+  method get_memory_address_wrapped_value: variable_t -> variable_t option
 
   (** {1 Predicates} *)
 
@@ -258,6 +260,8 @@ object
   method is_memory_variable: variable_t -> bool
   method is_string_literal_address: variable_t -> bool
   method is_memory_address: variable_t -> bool
+  method is_mut_memory_address: variable_t -> bool
+  method is_ref_memory_address: variable_t -> bool
   method is_fixed_xpr: xpr_t -> bool
   method is_initial_value: variable_t -> bool
   method is_initial_parameter_value: variable_t -> bool

CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml

@@ -664,7 +664,7 @@ object (self)
                  match memref#get_base with
                  | CStackAddress v -> v
                  | CGlobalAddress v -> v
-                 | CBaseVar (v, _, _) -> v
+                 | CBaseVar (v, _) -> v
                  | _ ->
                     raise
                       (CCHFailure

CodeHawk/CHC/cchanalyze/cCHNumericalConstraints.ml

@@ -36,7 +36,7 @@ open CHPretty
 open CHUtils
 
 (* cchlib *)
-open CCHUtilities
+(* open CCHUtilities *)
 
 (* cchanalyze *)
 open CCHAnalysisTypes
@@ -133,7 +133,7 @@ object (self)
 	    let _ =
               if coeff1#equal numerical_zero || coeff2#equal numerical_zero then
 		raise
-                  (CCHFailure
+                  (CHCommon.CHFailure
                      (LBLOCK [
                           STR "Internal error in elimination of ";
                           v#toPretty;

CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml

@@ -151,7 +151,7 @@ object (self)
        let deps = DLocal [invindex] in
        let msg = "address of stack variable: " ^ vinfo.vname in
        Some (deps,msg)
-    | CBaseVar (v, _, _) -> self#var_is_stack_memory invindex v
+    | CBaseVar (v, _) -> self#var_is_stack_memory invindex v
     | _ -> None
 
   method private var_is_stack_memory (invindex: int) (v: variable_t) =
@@ -413,7 +413,7 @@ object (self)
   method private memref_implies_delegation
                    (invindex: int) (memref: memory_reference_int) =
     match memref#get_base with
-    | CBaseVar (v, _, _) -> self#var_implies_delegation invindex v
+    | CBaseVar (v, _) -> self#var_implies_delegation invindex v
     | _ -> None
 
   method private var_implies_delegation (invindex: int) (v: variable_t) =

CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml

@@ -133,7 +133,7 @@ object (self)
        let (vinfo, offset) = poq#env#get_global_variable gvar in
        let msg = self#var_address_to_string vinfo offset in
        Some (deps, msg)
-    | CBaseVar (v, _, _) -> self#var_implies_safe invindex v
+    | CBaseVar (v, _) -> self#var_implies_safe invindex v
     | _ -> None
 
   method private var_implies_safe (invindex: int) (v: variable_t) =

CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml

@@ -175,7 +175,7 @@ object (self)
               let (memref, _offset) = poq#env#get_memory_address v in
               begin
                 match memref#get_base with
-                | CBaseVar (bv, _, _) ->
+                | CBaseVar (bv, _) ->
                    let _ =
                      poq#set_diagnostic_arg
                        arg ("base var: " ^ (p2s bv#toPretty)) in

CodeHawk/CHC/cchanalyze/cCHPOCheckIntUnderflow.ml

@@ -878,7 +878,7 @@ object (self)
               let (memref, _offset) = poq#env#get_memory_address v in
               begin
                 match memref#get_base with
-                | CBaseVar (bv, _, _) ->
+                | CBaseVar (bv, _) ->
                    let _ =
                      poq#set_diagnostic_arg
                        arg ("base var: " ^ (p2s bv#toPretty)) in

CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml

@@ -123,7 +123,7 @@ object (self)
          ^ vinfo.vname in
        let site = Some (__FILE__, __LINE__, mname) in
        Some (deps, msg, site)
-    | CBaseVar (bvar, _, _) ->
+    | CBaseVar (bvar, _) ->
        self#memlval_memref_basevar_implies_safe invindex bvar
     | _ ->
        begin

CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml

@@ -90,7 +90,7 @@ object (self)
        let (vinfo, _offset) = poq#env#get_local_variable svar in
        let msg = "address of stack variable: " ^ vinfo.vname in
        Some (deps, msg)
-    | CBaseVar (svar, _, _) ->
+    | CBaseVar (svar, _) ->
        let msg =
          "address of externally provided variable/field: "
          ^ svar#getName#getBaseName in
@@ -255,7 +255,7 @@ object (self)
               None
          | _ -> None
        end
-    | CBaseVar (v, _, _) ->
+    | CBaseVar (v, _) ->
        self#var_offset_implies_universal_violation invindex v xoffset
     | _ -> None
 

CodeHawk/CHC/cchanalyze/cCHPOCheckNoOverlap.ml

@@ -106,7 +106,7 @@ object (self)
       let memref = poq#env#get_memory_reference v in
       let _ = poq#set_diagnostic_arg arg (self#memref_to_string memref) in
       match memref#get_base with
-      | CBaseVar (basevar, _, _) -> self#is_alloca_address arg basevar invindex
+      | CBaseVar (basevar, _) -> self#is_alloca_address arg basevar invindex
       | _ -> None
     else
       None
@@ -135,7 +135,7 @@ object (self)
       let memref = poq#env#get_memory_reference v in
       let _ = poq#set_diagnostic_arg arg (self#memref_to_string memref) in
       match memref#get_base with
-      | CBaseVar (basevar, _, _) ->
+      | CBaseVar (basevar, _) ->
          if poq#is_api_expression (XVar basevar) then
            let xapi = poq#get_api_expression (XVar basevar) in
            let deps = DLocal [invindex] in