CHC: update Makefiles

Author: sipma

CodeHawk/CHC/cchanalyze/Makefile

@@ -61,6 +61,7 @@ MLIS := \
 	cCHPOCheckIndexLowerBound \
 	cCHPOCheckIndexUpperBound \
 	cCHPOCheckInitialized \
+	cCHPOCheckLocallyInitialized \
 	cCHPOCheckInitializedRange \
 	cCHPOCheckIntUtil \
 	cCHPOCheckIntOverflow \
@@ -72,6 +73,8 @@ MLIS := \
 	cCHPOCheckNotNull \
 	cCHPOCheckNotZero \
 	cCHPOCheckNonNegative \
+	cCHPOCheckOutputParameterInitialized \
+	cCHPOCheckOutputParameterUnaltered \
 	cCHPOCheckPreservedAllMemory \
 	cCHPOCheckStackAddressEscape \
 	cCHPOCheckWidthOverflow \
@@ -126,6 +129,7 @@ SOURCES := \
 	cCHPOCheckIndexLowerBound \
 	cCHPOCheckIndexUpperBound \
 	cCHPOCheckInitialized \
+	cCHPOCheckLocallyInitialized \
 	cCHPOCheckInitializedRange \
 	cCHPOCheckIntUtil \
 	cCHPOCheckIntOverflow \
@@ -138,6 +142,8 @@ SOURCES := \
 	cCHPOCheckNotZero \
 	cCHPOCheckNonNegative \
 	cCHPOCheckWidthOverflow \
+	cCHPOCheckOutputParameterInitialized \
+	cCHPOCheckOutputParameterUnaltered \
 	cCHPOCheckNullTerminated \
 	cCHPOCheckPointerCast \
 	cCHPOCheckPreservedAllMemory \

CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml

@@ -45,15 +45,17 @@ let _fenv = CCHFileEnvironment.file_environment
 
 
 class locally_initialized_checker_t
-        (_poq: po_query_int)
+        (poq: po_query_int)
         (vinfo: varinfo)
         (_lval: lval)
         (_invs: invariant_int list) =
-object
+object (self)
 
   method private vinfo = vinfo
 
-  method check_safe = false
+  method check_safe =
+    let _ = poq#set_vinfo_diagnostic_invariants self#vinfo in
+    false
 
   method check_violation = false
 

CodeHawk/CHC/cchpre/Makefile

@@ -65,6 +65,7 @@ MLIS := \
 	cCHPrimaryProofObligations \
 	cCHCheckValid \
 	cCHCreatePrimaryProofObligations \
+	cCHCreateOutputParameterPOs \
 
 CMIS := $(addprefix cmi/,$(MLIS:%=%.cmi))
 
@@ -100,6 +101,7 @@ SOURCES := \
 	cCHPrimaryProofObligations \
 	cCHCheckValid \
 	cCHCreatePrimaryProofObligations \
+	cCHCreateOutputParameterPOs \
 
 
 OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx))