CHT:CHC: update tests

Author: sipma

CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.ml

@@ -59,13 +59,15 @@ let unpack_tar_gz (predicate: string) (filename: string) =
   ()
 
 
-let analysis_setup ?(domains=default_domains) (predicate: string) (filename: string) =
+let analysis_setup
+      ?(domains=default_domains) (predicate: string) (filename: string) =
   begin
     unpack_tar_gz predicate filename;
     system_settings#set_projectname filename;
     system_settings#set_cfilename filename;
     (if system_settings#is_output_parameter_analysis then
-       CCHCreateOutputParameterPOs.output_parameter_po_process_file ()
+       CHTraceResult.tget_ok
+         (CCHCreateOutputParameterPOs.output_parameter_po_process_file ())
      else
        CCHCreatePrimaryProofObligations.primary_process_file ());
     CCHProofScaffolding.proof_scaffolding#reset;

CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.mli

@@ -76,7 +76,8 @@
     - generate invariants and run the proof obligation checkers for the proof
       obligation present.
  *)
-val analysis_setup: ?domains:string list -> string -> string -> unit
+val analysis_setup:
+  ?domains:string list -> string -> string -> unit CHTraceResult.traceresult
 
 
 (** [analysis_take_down filename] removes the directory [filename.cch] from

CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml

@@ -110,12 +110,12 @@ let check_violation () =
       ("rl-memlval-001",
        "locally_initialized_rl_memlval_001", "rl_memlval_001",
        [], -1, -1,
-       "memlval_vinv_implies_violation",
+       "memlval_implies_violation",
        "initialized from parameter p->fld1 with offset .fld1");
       ("rl-memlval-002",
        "locally_initialized_rl_memlval_002", "rl_memlval_002",
        [], -1, -1,
-       "memlval_vinv_implies_violation",
+       "memlval_implies_violation",
        "initialized from parameter p->fld1 with offset .fld1")
     ] in
   begin