CHC: fix for regression-test failure

static-analysis-engineering · Sep 16, 2024 · 7d5372d · 7d5372d
1 parent 07b782c
commit 7d5372d
Show file tree

Hide file tree

Showing 11 changed files with 130 additions and 71 deletions.
diff --git a/CodeHawk/CHC/cchanalyze/cCHAnalyze.ml b/CodeHawk/CHC/cchanalyze/cCHAnalyze.ml
@@ -76,7 +76,7 @@ let analyze_procedure_with_intervals (proc:procedure_int) (system:system_int)
     analysis_setup#addDomain intervals_domain (new intervals_domain_no_arrays_t);
     analysis_setup#setOpSemantics (semantics intervals_domain);
     analysis_setup#analyze_procedure system proc;
-    log_info "Interval analysis completed"
+    log_info "Interval analysis completed [%s:%d]" __FILE__ __LINE__
   end
 
 
@@ -93,7 +93,7 @@ let analyze_procedure_with_pepr
       pepr_domain (mk_pepr_domain_no_arrays params timeout);
     analysis_setup#setOpSemantics (semantics pepr_domain);
     analysis_setup#analyze_procedure system proc;
-    log_info "Pepr analysis completed"
+    log_info "Pepr analysis completed [%s:%d]" __FILE__ __LINE__
   end
 
 
@@ -105,7 +105,7 @@ let analyze_procedure_with_valuesets (proc:procedure_int) (system:system_int)
     analysis_setup#addDomain valueset_domain (new valueset_domain_no_arrays_t);
     analysis_setup#setOpSemantics (semantics valueset_domain);
     analysis_setup#analyze_procedure system proc;
-    log_info "Value set analysis completed"
+    log_info "Value set analysis completed [%s:%d]" __FILE__ __LINE__
   end
 
 
@@ -120,7 +120,7 @@ let analyze_procedure_with_linear_equalities
         linear_equalities_domain (new linear_equalities_domain_no_arrays_t);
       analysis_setup#setOpSemantics (semantics linear_equalities_domain);
       analysis_setup#analyze_procedure system proc;
-      log_info "Linear equality analysis completed"
+      log_info "Linear equality analysis completed [%s:%d]" __FILE__ __LINE__
     end
   with
   | CHFailure p ->
@@ -142,7 +142,7 @@ let analyze_procedure_with_symbolic_sets (proc:procedure_int) (system:system_int
       symbolic_sets_domain (new symbolic_sets_domain_no_arrays_t);
     analysis_setup#setOpSemantics (semantics symbolic_sets_domain);
     analysis_setup#analyze_procedure system proc;
-    log_info "symbolic sets analysis completed"
+    log_info "symbolic sets analysis completed [%s:%d]" __FILE__ __LINE__
   end
 
 
@@ -173,7 +173,7 @@ let analyze_procedure_with_sym_pointersets
       sym_pointersets_domain (new timed_symbolic_sets_domain_no_arrays_t timeout);
     analysis_setup#setOpSemantics (semantics sym_pointersets_domain);
     analysis_setup#analyze_procedure system proc;
-    log_info "symbolic pointerset analysis completed"
+    log_info "symbolic pointerset analysis completed [%s:%d]" __FILE__ __LINE__
   end
 
 

diff --git a/CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml b/CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml
@@ -162,7 +162,7 @@ let make_invariant_generation_spec t =
 let process_function gspecs fname =
   try
     if !function_to_be_analyzed = fname || !function_to_be_analyzed = "" then
-      let _ = log_info "analyze function %s" fname in
+      let _ = log_info "analyze function %s [%s:%d]" fname __FILE__ __LINE__ in
       let fundec = read_function_semantics fname in
       let fdecls = fundec.sdecls in
       let _ = read_proof_files fname fdecls in
@@ -175,9 +175,10 @@ let process_function gspecs fname =
       let openpos = List.filter (fun po -> not po#is_closed) proofObligations in
       let _ =
         log_info
-          "Obtained %d proof obligation(s) of which %d open"
+          "Obtained %d proof obligation(s) of which %d open [%s:%d]"
           (List.length proofObligations)
-          (List.length openpos) in
+          (List.length openpos)
+          __FILE__ __LINE__ in
       if (List.length openpos) > 0 then
         let callcount = proof_scaffolding#get_call_count fname in
         let _ =
@@ -286,7 +287,7 @@ let process_function gspecs fname =
       let env = mk_c_environment fundec varmgr in
       begin
         check_proof_obligations env fnApi invio proofObligations;
-        log_info "checked proof obligations";
+        log_info "checked proof obligations [%s:%d]" __FILE__ __LINE__;
         save_invs fname invio;
         save_vars fname varmgr;
         save_proof_files fname;
@@ -350,16 +351,18 @@ let generate_and_check_process_file (domains: string list) =
     let _ = read_cfile_assignment_dictionary () in
     let _ = read_cfile_contract () in
     let _ = file_contract#collect_file_attributes in
-    let _ = log_info "Read file-level xml files" in
+    let _ = log_info "Read file-level xml files [%s:%d]" __FILE__ __LINE__ in
     let functions = fenv#get_application_functions in
-    let _ = log_info "Processing %d functions" (List.length functions) in
+    let _ =
+      log_info "Processing %d functions [%s:%d]"
+        (List.length functions) __FILE__ __LINE__ in
     let _ = List.iter (fun f -> process_function gspecs f.vname) functions in
     let _ = save_cfile_assignment_dictionary () in
     let _ = save_cfile_dictionary () in
     let _ = save_cfile_context () in
     let _ = save_cfile_interface_dictionary () in
     let _ = save_cfile_predicate_dictionary () in
-    let _ = log_info "Saved file-level xml files" in
+    let _ = log_info "Saved file-level xml files [%s:%d]" __FILE__ __LINE__ in
     ()
   with
   | CHXmlReader.IllFormed ->

diff --git a/CodeHawk/CHC/cchcil/cCHXParseFile.ml b/CodeHawk/CHC/cchcil/cCHXParseFile.ml
@@ -86,7 +86,9 @@ let check_targetdirectory () =
   if !targetdirectory = "" then
     begin
       log_warning
-        "Target directory not set: using current directory as target directory";
+        ("Target directory not set: using current directory as target "
+         ^^ "directory [%s:%d]")
+        __FILE__ __LINE__;
       targetdirectory := Sys.getcwd ()
     end
 
@@ -114,7 +116,9 @@ let sanitize_targetfilename name =
     let newname =
       (String.sub name 0 (spos2+1))
       ^ (String.sub name (pos+2) ((String.length name) - (pos+2))) in
-    let _ = log_info "Change name from %s into %s" name newname in
+    let _ =
+      log_info "Change name from %s into %s [%s:%d]"
+        name newname __FILE__ __LINE__ in
     newname
   with
     Not_found -> name
@@ -222,7 +226,7 @@ let cil_function_to_file target (f: fundec) (dir: string) =
     write_xml_function_definition functionNode f target;
     root#appendChildren [functionNode];
     file_output#saveFile ffilename doc#toPretty;
-    log_info "Saved function file %s" ffilename
+    log_info "Saved function file %s [%s:%d]" ffilename __FILE__ __LINE__
   end
 
 

diff --git a/CodeHawk/CHC/cchcil/cHCilDeclarations.ml b/CodeHawk/CHC/cchcil/cHCilDeclarations.ml
@@ -124,9 +124,10 @@ object (self)
     | Error e ->
        begin
          log_error
-             "index_varinfo: %s; %s"
+             "index_varinfo: %s; %s [%s:%d]"
              vinfo.vname
-             (String.concat ", " e);
+             (String.concat ", " e)
+             __FILE__ __LINE__;
          raise
            (CHFailure
               (LBLOCK [
@@ -152,9 +153,10 @@ object (self)
     | Error e ->
        begin
          log_error
-           "index fieldinfo: %s %s"
+           "index fieldinfo: %s %s [%s:%d]"
            finfo.fname
-           (String.concat ", " e);
+           (String.concat ", " e)
+           __FILE__ __LINE__;
          raise
            (CHFailure
               (LBLOCK [
@@ -183,9 +185,10 @@ object (self)
     | Error e ->
        begin
          log_error
-           "index enumitem: %s %s"
+           "index enumitem: %s %s [%s:%d]"
            name
-           (String.concat ", " e);
+           (String.concat ", " e)
+           __FILE__ __LINE__;
          raise
            (CHFailure
               (LBLOCK [

diff --git a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml
@@ -172,35 +172,42 @@ let main () =
     else if !cmd = "primary" then
       begin
 	primary_process_file ();
-        log_info "primary proof obligations generated";
+        log_info "primary proof obligations generated [%s:%d]" __FILE__ __LINE__;
 	save_log_files "primary";
-        log_info "primary proof obligations log files saved"
+        log_info
+          "primary proof obligations log files saved [%s:%d]" __FILE__ __LINE__
       end
 
     else if !cmd = "localinvs" then
       begin
 	invariants_process_file (List.rev !domains);
-        log_info "Local invariants generated";
+        log_info "Local invariants generated [%s:%d]" __FILE__ __LINE__;
 	save_log_files "localinvs";
-        log_info "Local invariant generation log files saved"
+        log_info
+          "Local invariant generation log files saved [%s:%d]" __FILE__ __LINE__
       end
 
     else if !cmd = "globalinvs" then ()
 
     else if !cmd = "check" then
       begin
 	check_process_file ();
-        log_info "Proof obligations checked";
+        log_info "Proof obligations checked [%s:%d" __FILE__ __LINE__;
 	save_log_files "check";
-        log_info "Proof obligation checking log files saved"
+        log_info
+          "Proof obligation checking log files saved [%s:%d]" __FILE__ __LINE__
       end
 
     else if !cmd = "generate_and_check" then
       begin
         generate_and_check_process_file (List.rev !domains);
-        log_info "Invariants generated and proof obligations checked";
+        log_info
+          "Invariants generated and proof obligations checked [%s:%d]"
+          __FILE__ __LINE__;
         save_log_files "gencheck";
-        log_info "Invariant generation and proof obligation check log files saved"
+        log_info
+          "Invariant generation and proof obligation check log files saved [%s:%d]"
+          __FILE__ __LINE__
       end
 
     else

diff --git a/CodeHawk/CHC/cchlib/cCHCAttributes.ml b/CodeHawk/CHC/cchlib/cCHCAttributes.ml
@@ -62,9 +62,11 @@ let convert_attribute_to_function_conditions
         | _  ->
            begin
              log_info
-               "attribute conversion for %s: attribute parameters %s not recognized"
+               ("attribute conversion for %s: attribute parameters %s not "
+                ^^ "recognized [%s:%d]")
                name
-               (String.concat ", " (List.map attrparam_to_string attrparams));
+               (String.concat ", " (List.map attrparam_to_string attrparams))
+               __FILE__ __LINE__;
              ([], [])
            end) in
 
@@ -83,9 +85,11 @@ let convert_attribute_to_function_conditions
         | _ ->
            begin
              log_info
-               "attribute conversion for %s: attribute parameters %s not recognized"
+               ("attribute conversion for %s: attribute parameters %s not "
+                ^^ "recognized [%s:%d]")
                name
-               (String.concat ", " (List.map attrparam_to_string attrparams));
+               (String.concat ", " (List.map attrparam_to_string attrparams))
+               __FILE__ __LINE__;
              []
            end) in
      (pre, [], [])
@@ -102,9 +106,11 @@ let convert_attribute_to_function_conditions
         | _ ->
            begin
              log_info
-               "attribute conversion for %s: attribute parameters %s not recognized"
+               ("attribute conversion for %s: attribute parameters %s not "
+                  ^^ "recognized [%s:%d]")
                name
-               (String.concat ", " (List.map attrparam_to_string attrparams));
+               (String.concat ", " (List.map attrparam_to_string attrparams))
+               __FILE__ __LINE__;
              []
            end) in
      ([], post, [])
@@ -118,9 +124,10 @@ let convert_attribute_to_function_conditions
               begin
                 log_info
                   ("attribute conversion for %s: parameter %s not recognized "
-                   ^^ "(excluded)")
+                   ^^ "(excluded) [%s:%d]")
                   name
-                  (attrparam_to_string attrparam);
+                  (attrparam_to_string attrparam)
+                  __FILE__ __LINE__;
                 acc
               end) [] attrparams in
      (pre, [], [])
@@ -137,9 +144,10 @@ let convert_attribute_to_function_conditions
               begin
                 log_info
                   ("attribute conversion for %s: parameter %s not recognized "
-                   ^^ "(excluded)")
+                   ^^ "(excluded) [%s:%d]")
                   name
-                  (attrparam_to_string attrparam);
+                  (attrparam_to_string attrparam)
+                  __FILE__ __LINE__;
                 acc
               end) [] attrparams in
      (pre, [], [])
@@ -165,9 +173,10 @@ let convert_attribute_to_function_conditions
               begin
                 log_info
                   ("attribute conversion for %s: parameter %s not recognized "
-                   ^^ "(excluded)")
+                   ^^ "(excluded) [%s:%d]")
                   name
-                  (attrparam_to_string attrparam);
+                  (attrparam_to_string attrparam)
+                  __FILE__ __LINE__;
                 acc
               end) [] attrparams in
      ([], [], se)
@@ -188,8 +197,10 @@ let attribute_update_globalvar_contract
   | Attr ("chkc_not_null", []) -> gvarc#set_not_null
   | Attr (s, attrparams) ->
      log_info
-       "global variable attribute %s for %s with %d parameters not recognized"
+       ("global variable attribute %s for %s with %d parameters not "
+        ^^ "recognized [%s:%d]")
        s
        gvarc#get_name
        (List.length attrparams)
+       __FILE__ __LINE__