4. Analysis support definition

After this step, the user must define the data type that will be used as the analysis support. The whole expressive power of ocaml is here available: it is so possible to define data strucutures as complex as needed. MURZ, furthermore, features some prepackaged useful data structures, ready to use, as variables and expressions sets, lifted lattice of constant integers, labelled commands sets. In our running example, the analysis support is the set of variables. We define explicitly top, bottom ³, and init. We remind that top must be the neutral element of meet, and that init is the value that will be used to initialize the information on every node in the CFG.

module LiveCarrier =  
   struct

(* support of the analysis *)

   type t = VarSet.t

   let top = ref VarSet.empty
   let bottom = top
   let init = top

In some cases, the analysis needs to initialize some of these data to values known only at run-time: the function do_init will be used to accomplish this task. As an example, see verybusy.ml:

   type t = ExpressionSet.t
   let top = ref ExpressionSet.empty
   let do_init (cfg) = top := calcola_tutte_le_espressioni (cfg)
       (* compute the set all the expressions, in italian *)
   let bottom = ref (ExpressionSet.empty)
   let init = top

We remind that do_init is computed as a function of the program control-flow graph, and that it is called at the beginning of every analysis.

In this section of the module, some support variables can be defined. In our running example:

   let tutte_le_var = ref ( [] );; (* all the variables *)
   let do_init (cfg) = 
       tutte_le_var := calcola_tutte_le_variabili (cfg)
       (* compute the set of all the variables *)

A defintion of do_init is required. If not needed by a specific analysis, the user must definire a null function.

Last, the user must define a comparing function for two values in the support:

   let equal x y = VarSet.equal x y 

(* end of support definition *)