CHC: add invariant prioritization to the PLocallyInitialized checker

Author: sipma

CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml

@@ -278,7 +278,7 @@ object (self)
                | _ ->
                   let deps = DLocal [invindex; vinv#index] in
                   let msg =
-                    "local assignment(s) to "
+                    "assignment(s) to "
                     ^ vinfo.vname
                     ^ ": "
                     ^ (String.concat

CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml

@@ -249,7 +249,12 @@ end
 
 
 let check_locally_initialized (poq:po_query_int) (vinfo: varinfo) (lval:lval) =
-  let invs = poq#get_invariants 2 in
+  let f_priority (inv: invariant_int) =
+    match inv#get_fact with
+    | NonRelationalFact (_, FInitializedSet _) -> true
+    | _ -> false in
+  let invs =
+    CCHInvariantFact.prioritize_invariants f_priority (poq#get_invariants 2) in
   let _ = poq#set_diagnostic_invariants 2 in
   let _ =
     poq#set_init_vinfo_mem_diagnostic_invariants

CodeHawk/CHC/cchlib/cCHLibTypes.mli

@@ -873,6 +873,7 @@ class type system_settings_int =
     method is_value_wrap_around: bool
 
     method set_output_parameter_analysis: unit
+    method set_undefined_behavior_analysis: unit
     method is_undefined_behavior_analysis: bool
     method is_output_parameter_analysis: bool
 

CodeHawk/CHC/cchlib/cCHSettings.ml

@@ -98,7 +98,11 @@ object
 
   method is_value_wrap_around = analysis_level = ValueWrapAround
 
-  method set_output_parameter_analysis = analysis_kind <- OutputParameterAnalysis
+  method set_output_parameter_analysis =
+    analysis_kind <- OutputParameterAnalysis
+
+  method set_undefined_behavior_analysis =
+    analysis_kind <- UndefinedBehaviorAnalysis
 
   method is_undefined_behavior_analysis =
     analysis_kind = UndefinedBehaviorAnalysis