5  How to Use CIL

5.1  Using cilly, the CIL driver

1. Modify logwrites.ml so that it includes a CIL “feature descriptor” like this:

   let feature : featureDescr = 
     { fd_name = "logwrites";              
       fd_enabled = ref false;
       fd_description = "generation of code to log memory writes";
       fd_extraopt = [];
       fd_doit = 
       (function (f: file) -> 
         let lwVisitor = new logWriteVisitor in
         visitCilFileSameGlobals lwVisitor f)
     } 
   

   The fd_name field names the feature and its associated command-line arguments. The fd_enabled field is a bool ref. “fd_doit” will be invoked if !fd_enabled is true after argument parsing, so initialize the ref cell to true if you want this feature to be enabled by default.
   
   When the user passes the --dologwrites command-line option to cilly, the variable associated with the fd_enabled flag is set and the fd_doit function is called on the Cil.file that represents the merger (see Section 13) of all C files listed as arguments.
   
   
2. Invoke configure with the arguments

   ./configure EXTRASRCDIRS=/home/necula EXTRAFEATURES=logwrites
   

   This step works if each feature is packaged into its own ML file, and the name of the entry point in the file is feature.
   
   An alternative way to specify the new features is to change the build files yourself, as explained below. You'll need to use this method if a single feature is split across multiple files.
   1. Put logwrites.ml in the src or src/ext directory. This will make sure that make can find it. If you want to put it in some other directory, modify Makefile.in and add to SOURCEDIRS your directory. Alternately, you can create a symlink from src or src/ext to your file.
      
      
   2. Modify the Makefile.in and add your module to the CILLY_MODULES or CILLY_LIBRARY_MODULES variables. The order of the modules matters. Add your modules somewhere after cil and before main.
      
      
   3. If you have any helper files for your module, add those to the makefile in the same way. e.g.:

      CILLY_MODULES = $(CILLY_LIBRARY_MODULES) \
                      myutilities1 myutilities2 logwrites \
                      main
      

      Again, order is important: myutilities2.ml will be able to refer to Myutilities1 but not Logwrites. If you have any ocamllex or ocamlyacc files, add them to both CILLY_MODULES and either MLLS or MLYS.
      
      
   4. Modify main.ml so that your new feature descriptor appears in the global list of CIL features.

      let features : C.featureDescr list = 
        [ Logcalls.feature;
          Oneret.feature;    
          Heapify.feature1;  
          Heapify.feature2;
          makeCFGFeature; 
          Partial.feature;
          Simplemem.feature;
          Logwrites.feature;  (* add this line to include the logwrites feature! *)
        ] 
        @ Feature_config.features 
      

      Features are processed in the order they appear on this list. Put your feature last on the list if you plan to run any of CIL's built-in features (such as makeCFGfeature) before your own.
   
   Standard code in cilly takes care of adding command-line arguments, printing the description, and calling your function automatically. Note: do not worry about introducing new bugs into CIL by adding a single line to the feature list.
   
   
3. Now you can invoke the cilly application on a preprocessed file, or instead use the cilly driver which provides a convenient compiler-like interface to cilly. See Section 7 for details using cilly. Remember to enable your analysis by passing the right argument (e.g., --dologwrites).

5.2  Using CIL as a library

$ ocamlopt -c -I $(CIL)/obj/x86_LINUX/ main.ml
$ ocamlopt -ccopt -L$(CIL)/obj/x86_LINUX/ -o main unix.cmxa str.cmxa \ 
        $(CIL)/obj/x86_LINUX/cil.cmxa main.cmx