CHC: fix warnings and reformat

Author: sipma

CodeHawk/CHC/cchlib/cCHDeclarations.ml

@@ -41,7 +41,6 @@ open CHXmlDocument
 
 (* cchcil *)
 open CCHBasicTypes
-open CCHDictionary
 open CCHLibTypes
 open CCHSumTypeSerializer
 open CCHUtilities

CodeHawk/CHC/cchlib/cCHFunDeclarations.ml

@@ -1,23 +1,23 @@
 (* =============================================================================
-   CodeHawk C Analyzer 
+   CodeHawk C Analyzer
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
+
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2023 Aarno Labs LLC
+   Copyright (c) 2021-2024 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
    in the Software without restriction, including without limitation the rights
    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
    copies of the Software, and to permit persons to whom the Software is
    furnished to do so, subject to the following conditions:
- 
+
    The above copyright notice and this permission notice shall be included in all
    copies or substantial portions of the Software.
-  
+
    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -37,13 +37,12 @@ open CHXmlDocument
 (* cchlib *)
 open CCHBasicTypes
 open CCHFileEnvironment
-open CCHLibTypes
 open CCHSumTypeSerializer
 open CCHUtilities
 
 module H = Hashtbl
 
-   
+
 let cd = CCHDictionary.cdictionary
 let cdecls = CCHDeclarations.cdeclarations
 
@@ -136,7 +135,7 @@ object (self)
                  STR "Formal ";
                  INT n;
                  STR " not found in function declarations"]))
-    
+
   method get_locals =
     List.filter
       (fun vinfo -> vinfo.vparam = 0)
@@ -166,7 +165,7 @@ object (self)
                    STR "Global variable with name: ";
                    STR name;
                    STR " not found"]))
-      
+
   method get_varinfo_by_vid (vid:int) =
     if H.mem vidtable vid then
       self#xrep (varinfo_table#retrieve (H.find vidtable vid))
@@ -183,7 +182,7 @@ object (self)
     begin
       H.replace vidtable vinfo.vid index;
       index
-    end              
+    end
 
   method index_varinfo (vinfo:varinfo) =
     varinfo_table#add (self#getrep vinfo)
@@ -204,9 +203,8 @@ object (self)
         (List.map
            (fun (key,index) -> (index,self#xrep key)) varinfo_table#items)
     end
-    
+
 end
 
 
 let mk_cfundeclarations () = new cfundeclarations_t
-    

CodeHawk/CHC/cchlib/cCHLibTypes.mli

@@ -28,7 +28,6 @@
    ============================================================================= *)
 
 (* chlib *)
-open CHLanguage
 open CHNumerical
 open CHPretty
 
@@ -48,45 +47,45 @@ open CCHBasicTypes
  *)
 
 type machine_sizes_t = {
-  sizeof_short : xpr_t ;
-  sizeof_int   : xpr_t ;
-
-  sizeof_bool  : xpr_t ;
-  sizeof_long  : xpr_t ;
-
-  sizeof_longlong : xpr_t ;
-  sizeof_ptr      : xpr_t ;
-  sizeof_enum     : xpr_t ;
-  sizeof_float    : xpr_t ;
-  sizeof_double   : xpr_t ;
-
-  sizeof_longdouble  : xpr_t ;
-  sizeof_void        : xpr_t ;
-  sizeof_fun         : xpr_t ;
-
-  alignof_short  : xpr_t ;
-  alignof_int    : xpr_t ;
-  alignof_bool   : xpr_t ;
-  alignof_long   : xpr_t ;
-
-  alignof_longlong  : xpr_t ;
-  alignof_ptr       : xpr_t ;
-  alignof_enum      : xpr_t ;
-  alignof_float     : xpr_t ;
-
-  alignof_double    : xpr_t ;
-  alignof_longdouble: xpr_t ;
-  alignof_str       : xpr_t ;
-  alignof_fun       : xpr_t ;
-  alignof_aligned   : xpr_t ;
+  sizeof_short : xpr_t;
+  sizeof_int   : xpr_t;
+
+  sizeof_bool  : xpr_t;
+  sizeof_long  : xpr_t;
+
+  sizeof_longlong : xpr_t;
+  sizeof_ptr      : xpr_t;
+  sizeof_enum     : xpr_t;
+  sizeof_float    : xpr_t;
+  sizeof_double   : xpr_t;
+
+  sizeof_longdouble  : xpr_t;
+  sizeof_void        : xpr_t;
+  sizeof_fun         : xpr_t;
+
+  alignof_short  : xpr_t;
+  alignof_int    : xpr_t;
+  alignof_bool   : xpr_t;
+  alignof_long   : xpr_t;
+
+  alignof_longlong  : xpr_t;
+  alignof_ptr       : xpr_t;
+  alignof_enum      : xpr_t;
+  alignof_float     : xpr_t;
+
+  alignof_double    : xpr_t;
+  alignof_longdouble: xpr_t;
+  alignof_str       : xpr_t;
+  alignof_fun       : xpr_t;
+  alignof_aligned   : xpr_t;
 }
 
 type max_sizes_t = {
-  sizeof_int  : int ;
-  sizeof_float: int ;
-  sizeof_void : int ;
-  sizeof_ptr  : int ;
-  sizeof_fun  : int ;
+  sizeof_int  : int;
+  sizeof_float: int;
+  sizeof_void : int;
+  sizeof_ptr  : int;
+  sizeof_fun  : int;
   sizeof_enum : int
   }
 
@@ -510,18 +509,18 @@ type annotated_xpredicate_t = (xpredicate_t * summary_annotation_t)
 
 (* data structure condition *)
 type ds_condition_t = {
-    dsc_name: string ;
-    dsc_ckey : int ;
+    dsc_name: string;
+    dsc_ckey : int;
     dsc_fields : xpredicate_t list
   }
 
 type function_summary_t = {
-    fs_fname : string ;
+    fs_fname : string;
     fs_domainref: (string * string) option; (* specialized reasoning domain *)
-    fs_params : (string * int) list ;
-    fs_preconditions: annotated_xpredicate_t list ;
-    fs_postconditions: annotated_xpredicate_t list ;
-    fs_error_postconditions: annotated_xpredicate_t list ;
+    fs_params : (string * int) list;
+    fs_preconditions: annotated_xpredicate_t list;
+    fs_postconditions: annotated_xpredicate_t list;
+    fs_error_postconditions: annotated_xpredicate_t list;
     fs_sideeffects: annotated_xpredicate_t list
   }
 
@@ -601,8 +600,8 @@ type contract_instr_t =
   SetVar of int * s_term_t * s_term_t        (* line, lhs, rhs *)
 
 type contract_note_t = {
-    cn_tag: string ;
-    cn_prq: string ;
+    cn_tag: string;
+    cn_prq: string;
     cn_txt: string
   }
 
@@ -630,13 +629,13 @@ class type function_contract_int =
   end
 
 type contract_global_var_t = {
-    cgv_name: string ;
-    cgv_value: int option ;
-    cgv_lb: int option ;
-    cgv_ub: int option ;
-    cgv_static: bool ;
-    cgv_const: bool ;
-    cgv_notnull: bool ;
+    cgv_name: string;
+    cgv_value: int option;
+    cgv_lb: int option;
+    cgv_ub: int option;
+    cgv_static: bool;
+    cgv_const: bool;
+    cgv_notnull: bool;
     cgv_initialized_fields: string list
   }
 
@@ -671,11 +670,16 @@ class type global_contract_int =
 
 
 type analysis_level_t =
-  | UndefinedBehavior               (* only indicate undefined behavior (Red) *)
-  | ImplementationDefinedBehavior   (* indicate undefined behavior and implementation
-                                       defined behavior (Red,Purple) (default) *)
-  | ValueWrapAround  (* indicate undefined behavior, implementation-defined behavior,
-                        and value wrap around of unsigned integers (Red, Purple, Blue) *)
+  | UndefinedBehavior
+  (** only indicate undefined behavior (Red) *)
+
+  | ImplementationDefinedBehavior
+  (** indicate undefined behavior and implementation defined behavior
+      (Red,Purple) (default) *)
+
+  | ValueWrapAround
+  (** indicate undefined behavior, implementation-defined behavior, and value
+      wrap around of unsigned integers (Red, Purple, Blue) *)
 
 
 (** Paths and analysis options*)

CodeHawk/CHC/cchlib/cCHSettings.ml

@@ -30,9 +30,6 @@
 (* chlib *)
 open CHPretty
 
-(* chutil *)
-open CHTimingLog
-
 (* cchlib *)
 open CCHLibTypes
 open CCHUtilities

CodeHawk/CHC/cchpre/cCHCreatePrimaryProofObligations.ml

@@ -32,7 +32,6 @@ open CHPretty
 
 (* chutil *)
 open CHLogger
-open CHTiming
 open CHTimingLog
 
 (* cchlib *)

CodeHawk/CHC/cchpre/cCHPreFileIO.ml

@@ -34,7 +34,6 @@ open CHPretty
 open CHFileIO
 open CHLogger
 open CHPrettyUtil
-open CHTiming
 open CHTimingLog
 open CHXmlDocument
 open CHXmlReader
@@ -745,23 +744,7 @@ let read_target_files () =
 
 
 let get_cfile_basename ():string = ""
-                                     (*
-  try
-    Filename.concat
-      system_settings#get_path
-      (Filename.chop_extension system_settings#get_cfilename)
-  with
-  | _ ->
-    begin
-      ch_error_log#add
-        "chop extension" (LBLOCK [STR system_settings#get_cfilename]);
-      raise
-        (CCHFailure
-           (LBLOCK [
-                STR "Failed to find file : ";
-                STR (system_settings#get_cfilename)] ))
-    end
-                                      *)
+
 
 let get_contractfile_basename ():string =
   try
@@ -784,16 +767,7 @@ let  get_global_contract_filename ():string =
 
 
 let get_src_directory ():string = ""
-                                    (*
-  try
-    let semantics_dir = (Filename.dirname system_settings#get_path) in
-    (Filename.concat semantics_dir "sourcefiles")
-  with
-  | _ ->
-    begin
-      raise (CCHFailure (STR "get src directory"))
-    end
-                                     *)
+
 
 let save_cfile_logfile
       (log:logger_int) (contenttype:string) (logtype:string) =
@@ -805,10 +779,7 @@ let save_cfile_logfile
 
 
 let get_xml_summaryresults_name () = ""
-                                       (*
-  Filename.dirname
-    (Filename.dirname (system_settings#get_path)) ^ "/summaryresults.xml"
-                                        *)
+
 
 let get_xml_file_contract_name () =
   (get_contractfile_basename ()) ^ "_c.xml"

CodeHawk/CHC/cchpre/cCHPreFileIO.mli

@@ -182,4 +182,5 @@ val save_cfile_logfile: logger_int -> string -> string -> unit
 val get_xml_summaryresults_name: unit -> string
 val read_cfile_contract: unit -> unit
 val save_cfile_contract: unit -> unit
-                                   (* val get_xml_cfile: string -> file *)
+val get_savedsource_path: unit -> string
+val get_cfile_basename: unit -> string