CHC: set type of analysis

Author: sipma

CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml

@@ -187,6 +187,7 @@ let main () =
 
     else if !cmd = "outputparameters-primary" then
       begin
+        system_settings#set_output_parameter_analysis;
 	CCHCreateOutputParameterPOs.output_parameter_po_process_file ();
         log_info "primary proof obligations generated [%s:%d]" __FILE__ __LINE__;
 	save_log_files "primary";

CodeHawk/CHC/cchlib/cCHLibTypes.mli

@@ -788,6 +788,11 @@ class type global_contract_int =
 (** {1 System settings} *)
 
 
+type analysis_kind_t =
+  | UndefinedBehaviorAnalysis
+  | OutputParameterAnalysis
+
+
 type analysis_level_t =
   | UndefinedBehavior
   (** only indicate undefined behavior (Red) *)
@@ -867,6 +872,10 @@ class type system_settings_int =
     method is_implementation_defined: bool
     method is_value_wrap_around: bool
 
+    method set_output_parameter_analysis: unit
+    method is_undefined_behavior_analysis: bool
+    method is_output_parameter_analysis: bool
+
     (** {1 Other settings} *)
 
     method set_verbose: bool -> unit

CodeHawk/CHC/cchlib/cCHSettings.ml

@@ -50,6 +50,7 @@ object
   val mutable wordsize = Some 32
   val mutable use_unreachability = false
   val mutable analysis_level = ImplementationDefinedBehavior
+  val mutable analysis_kind = UndefinedBehaviorAnalysis
 
   method set_projectpath (p: string) = projectpath <- p
   method get_projectpath = projectpath
@@ -97,6 +98,14 @@ object
 
   method is_value_wrap_around = analysis_level = ValueWrapAround
 
+  method set_output_parameter_analysis = analysis_kind <- OutputParameterAnalysis
+
+  method is_undefined_behavior_analysis =
+    analysis_kind = UndefinedBehaviorAnalysis
+
+  method is_output_parameter_analysis =
+    analysis_kind = OutputParameterAnalysis
+
   method use_unreachability = use_unreachability
   method verbose = verbose