CHC: add global-variable attributes

Author: sipma

CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml

@@ -45,7 +45,6 @@ open CCHBasicTypes
 open CCHContext
 open CCHFileContract
 open CCHFileEnvironment
-open CCHLibTypes
 open CCHTypesTransformer
 open CCHTypesUtil
 
@@ -113,17 +112,17 @@ object (self)
         | _ -> acc) [] formals
 
   method private assert_global_values globals =
-    let contractgvars = file_contract#get_global_variables in
+    let contractgvars = file_contract#get_globalvar_contracts in
     let table = H.create 3 in
     let tmpProvider = (fun () -> env#mk_num_temp) in
     let cstProvider = (fun (n:numerical_t) -> env#mk_num_constant n) in
-    let _ = List.iter (fun gv -> H.add table gv.cgv_name gv) contractgvars in
+    let _ = List.iter (fun gv -> H.add table gv#get_name gv) contractgvars in
     let _ = env#start_transaction in
     let ccmds =
       List.fold_left (fun acc (vname, _, _, vInit) ->
           if H.mem table vname then
             let gcvar = H.find table vname in
-            match gcvar.cgv_value with
+            match gcvar#get_value with
             | Some i ->
                let x = XOp (XEq, [XVar vInit ; int_constant_expr i]) in
                let (code,bExp) = xpr2boolexpr tmpProvider cstProvider x in
@@ -142,10 +141,10 @@ object (self)
     let globalvars =
       List.map f.sdecls#get_varinfo_by_vid (get_block_variables f.sbody) in
     let globalvars = List.filter (fun vinfo -> vinfo.vglob) globalvars in
-    let contractglobals = file_contract#get_global_variables in
+    let contractglobals = file_contract#get_globalvar_contracts in
     let contractglobals =
       List.map (fun v ->
-          file_environment#get_globalvar_by_name v.cgv_name) contractglobals in
+          file_environment#get_globalvar_by_name v#get_name) contractglobals in
     let globalvars =
       List.fold_left (fun acc v ->
           if List.exists (fun vv ->
@@ -276,10 +275,10 @@ let get_valueset_preamble (env:c_environment_int) fundec =
     List.map (fun v ->
         (false,env#mk_formal_ptr_base_variable v NUM_VAR_TYPE)) pointerFormals in
   let contractglobals =
-    List.filter (fun v -> v.cgv_notnull) file_contract#get_global_variables in
+    List.filter (fun v -> v#is_not_null) file_contract#get_globalvar_contracts in
   let contractglobals =
     List.map (fun v ->
-        file_environment#get_globalvar_by_name v.cgv_name) contractglobals in
+        file_environment#get_globalvar_by_name v#get_name) contractglobals in
   let contractglobals =
     List.map (fun v ->
         (true,env#mk_program_var v NoOffset NUM_VAR_TYPE)) contractglobals in

CodeHawk/CHC/cchanalyze/cCHPOQuery.ml

@@ -434,7 +434,8 @@ object (self)
     match facts with
     | [] ->
        begin
-         self#set_diagnostic
+         self#set_diagnostic_arg
+           argindex
            ("no invariant facts in proof obligation context");
          []
        end
@@ -454,8 +455,9 @@ object (self)
        match vars with
        | [] ->
           begin
-            self#set_diagnostic
-              ("no invariants found on variables that apply to proof obligation");
+            self#set_diagnostic_arg
+              argindex
+              "no corresponding variables with non-relational facts";
             []
           end
        | _ ->
@@ -470,7 +472,8 @@ object (self)
           match invs with
           | [] ->
              begin
-               self#set_diagnostic
+               self#set_diagnostic_arg
+                 argindex
                  ("none of the variables has associated invariants: "
                   ^ (p2s
                        (pretty_print_list vars (fun v -> v#toPretty) "[" "," "]")));
@@ -1258,10 +1261,18 @@ object (self)
   method get_num_value (e:exp) = get_num_value fenv e
 
   method get_gv_lowerbound (name:string):int option =
-    file_contract#get_gv_lower_bound name
+    if file_contract#has_globalvar_contract name then
+      let gvar = file_contract#get_globalvar_contract name in
+      gvar#get_lower_bound
+    else
+      None
 
   method get_gv_upperbound (name:string):int option =
-    file_contract#get_gv_upper_bound name
+    if file_contract#has_globalvar_contract name then
+      let gvar = file_contract#get_globalvar_contract name in
+      gvar#get_upper_bound
+    else
+      None
 
   (* return a lower bound xpr *)
   method get_lowerbound_xpr (arg:int) (e:exp):(xpr_t * int list) option =