cosmetic changes from Julian (on options, loopfree Callstring and cal…

…lstring analyses)

src/analyses/callstring.ml

@@ -35,7 +35,7 @@ struct
         if get_int "ana.context.callString_length" < 0
         then new_callstr (* infinite call string *)
         else (* maximum of k elements *)
-          match (BatDeque.size new_callstr - (get_int "ana.context.callString_length")) with
+          match BatDeque.size new_callstr - (get_int "ana.context.callString_length") with
           | 1 -> fst @@ Option.get (BatDeque.rear new_callstr)
           | x when x <= 0 -> new_callstr
           | _ -> failwith "CallString Error: It shouldn't happen that more than one element must be deleted to maintain the correct height!"
@@ -67,7 +67,7 @@ struct
 end
 
 (* implementations of CallstringTypes*)
-module Callstring:CallstringType = struct
+module Callstring: CallstringType = struct
   include CilType.Fundec
   let ana_name = "string"
   let new_ele f ctx = 
@@ -77,7 +77,7 @@ module Callstring:CallstringType = struct
     else Some f'
 end
 
-module Callsite:CallstringType = struct
+module Callsite: CallstringType = struct
   include CilType.Stmt
   let ana_name = "site"
   let new_ele f ctx = 

src/analyses/loopfreeCallstring.ml

@@ -20,7 +20,7 @@ struct
   module FundecSet = SetDomain.Make (CilType.Fundec)
   module Either =  Printable.Either (CilType.Fundec) (FundecSet) 
 
-  module D = Lattice.Flat (Printable.Liszt (Either)) (* should be a List containing Sets of Fundecs and Fundecs. Lattice.Flat is used to fulfill the type *) 
+  module D = Lattice.Flat (Printable.Liszt (Either)) (* A domain element is a list containing fundecs and sets of fundecs.*) 
   module C = D
   module V = EmptyV
   module G = Lattice.Unit

src/config/options.schema.json

@@ -356,14 +356,14 @@
         },
         "ctx_insens": {
           "title": "ana.ctx_insens",
-          "description": "List of context-insensitive analyses, which is ignored if `ctx_sens` is not empty.",
+          "description": "List of context-insensitive analyses. This setting is ignored if `ana.ctx_sens` contains elements.",
           "type": "array",
           "items": { "type": "string" },
           "default": [ "stack_loc", "stack_trace_set" ]
         },
         "ctx_sens": {
           "title": "ana.ctx_sens",
-          "description": "List of context-sensitive analyses. In case of an empty array `ctx_insens` is used, otherwise `ctx_insens` is ignored.",
+          "description": "List of context-sensitive analyses. In case this list is empty, `ana.ctx_insens` will be used to determine the set of context-insensitive analyses.",
           "type": "array",
           "items": { "type": "string" },
           "default": []
@@ -980,13 +980,13 @@
             },
             "gas_value": {
               "title": "ana.context.gas_value",
-              "description": "x denotes the gas value for the ContextGasLifter. Negative value means deactivated, zero means context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitive, the remaining with no context.",
+              "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.",
               "type": "integer",
               "default": -1
             },
             "callString_length": {
               "title": "ana.context.callString_length",
-              "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to be effective, one analysis of the `callstring.ml` file must be activated.",
+              "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.",
               "type": "integer",
               "default": 2
             }