Commits

Zachary Anderson  committed 417e627

Bug fix in ciltutoptions.ml

  • Participants
  • Parent commits 6db69d5

Comments (0)

Files changed (13)

 . theorem provers (e.g. alt-ergo)
 . pass --disable-tut11 to the configure script to disable tut11
 
-After untarring the archive, enter the directory and do the following:
+After obtaining the code, enter the directory and do the following:
 
 $ ./configure
 $ make

File ciltut-lib/src/tut6.c

+
+
+
+
+
 
 
 
 
 #include <ciltut.h>
 
+
+
+
+
+
+
+
 int (*pthread_mutex_lock_orig)  (pthread_mutex_t *m) = NULL;
 int (*pthread_mutex_unlock_orig)(pthread_mutex_t *m) = NULL;
 
-CONSTRUCTOR static void wrapper_init()
-{
-  pthread_mutex_lock_orig   = checked_dlsym(RTLD_NEXT, "pthread_mutex_lock");
-  pthread_mutex_unlock_orig = checked_dlsym(RTLD_NEXT, "pthread_mutex_unlock");
-}
+
+
+
+
+
+
+
+
+
+
+
+
+
 
 int pthread_mutex_lock(pthread_mutex_t *m)
 {
   int res;
+  if (!pthread_mutex_lock_orig)
+    pthread_mutex_lock_orig = checked_dlsym(RTLD_NEXT, "pthread_mutex_lock");
   res = pthread_mutex_lock_orig(m);
   printf("thread: %d - pthread_mutex_lock(%p)\n", gettid(), m);
   fflush(stdout);
 int pthread_mutex_unlock(pthread_mutex_t *m)
 {
   int res;
+  if (!pthread_mutex_unlock_orig)
+    pthread_mutex_unlock_orig = checked_dlsym(RTLD_NEXT, "pthread_mutex_unlock");
   printf("thread: %d - pthread_mutex_unlock(%p)\n", gettid(), m);
   fflush(stdout);
   res = pthread_mutex_unlock_orig(m);
   return res;
 }
 
-

File src/ciltutoptions.ml

 
   
   "", Arg.Unit (fun () -> ()), "General:";
+  "--out", Arg.Set_string outFile, "Set the name of the output file";
+  "--home", Arg.Set_string home, "Set the name of ciltut's home directory";
   "--verbose", Arg.Set verbose,
     "Enable verbose output";
   "--stats", Arg.Set stats,
-
 
 
 
 module E = Errormsg 
 
 
-
 let tut0 (f : file) : unit =
   E.log "I could change %s if I wanted to!\n" f.fileName;
   ()
   f.globals
 
 
+

File src/tut10.ml

   | _ -> None
 
 
-
-
-
-
 type functions = {
   mutable cache_begin : varinfo;
   mutable cache_end   : varinfo;

File src/tut11.ml

   itimes_op : T.lsymbol; 
   idiv_op   : T.lsymbol; 
   imod_op   : T.lsymbol; 
-  lt_op    : T.lsymbol; 
-  gt_op    : T.lsymbol;
-  lte_op   : T.lsymbol;
-  gte_op   : T.lsymbol;
-  get_op   : T.lsymbol; 
-  set_op   : T.lsymbol;
+  lt_op     : T.lsymbol; 
+  gt_op     : T.lsymbol;
+  lte_op    : T.lsymbol;
+  gte_op    : T.lsymbol;
+  get_op    : T.lsymbol; 
+  set_op    : T.lsymbol;
 }
 
 
 let debug = ref false
 
 
-
-
-
-
 type oekind = Top | Odd | Even | Bottom
 
 
 let kind_of_vm (vm : varmap) : oekind  = vm |> snd |> snd
 
 
-
 let string_of_oekind (k : oekind) : string =
   match k with
   | Top    -> "Top"
   vml |> string_of_varmap_list |> text
 
 
-
-
-
-
 let oekind_neg (k : oekind) : oekind =
   match k with
   | Even -> Odd
   vm :: (L.remove_assoc (id_of_vm vm) vml)
 
 
-
-
-
-
 let kind_of_int64 (i : Int64.t) : oekind =
   let firstbit = Int64.logand i Int64.one in
   if firstbit = Int64.one then Odd else Even
 
 
 
-
-
 let varmap_list_kill (vml : varmap list) : varmap list =
   L.map (fun (vid, (vi, k)) ->
     if vi.vaddrof then (vid, (vi, Top)) else (vid, (vi, k)))
 module OddEven = DF.ForwardsDataFlow(OddEvenDF)
 
 
-
-
 let collectVars (fd : fundec) : varmap list =
   (fd.sformals @ fd.slocals)
   |> L.filter (fun vi -> isIntegralType vi.vtype)
     E.error "No data for first statement? %s" fd.svar.vname
 
 
-
-
-
-
-
-
 let getOddEvens (sid : int) : varmap list option =
   try Some(IH.find OddEvenDF.stmtStartData sid)
   with Not_found -> None
   else []
 
 
+
+
 and zeroField (fd : fundec) (blv : lval) (fi : fieldinfo) : stmt list =
   zeroType fd (addOffsetLval (Field(fi,NoOffset)) blv)
 
 open Cil
 
 let tut6 (f : file) : unit = ()
+
+
 module Q  = Queue
 
 module T = Tut7 
-
 type colors = T.color list 
 
 
       end else t
     in
     ChangeDoChildrenPost(t, action)
-
 end
 
 class typeNodeEraser = object(self)
+
+
+
+
+
+
+
+
+
 #include <stdio.h>
 
 int bar = 37;
 int foo()
 {
   int l;
-
   bar = 0;
   l = bar;
-
   return l;
 }
 
 int main()
 {
   int r;
-
   r = foo();
-
   printf("r = %d\n", r);
-
   return 0;
 }
 
+//@highlight \section{\texttt{test/tut3.c}}
+//@highlight \hltscom{The result of the analysis in \ttt{tut3.ml} will be to
+//@highlight    print a message to the console for each variable of integral
+//@highlight    type wherever it is used indicating whether it is even or odd
+//@highlight    at that program point. We consider the results of the analysis
+//@highlight    on the code below:}
+//@highlight \hlbegincode{}
+
+#include <stdio.h>
+
+int main()
+{
+  int a,b,c,d;
+  a = 1; b = 2; c = 3; d = 4;
+  a += b + c;
+  c *= d - b;
+  b -= d + a;
+  if (a % 2) a++;
+  printf("a = %d, b = %d, c = %d, d = %d\n", a, b, c, d);
+  return 0;
+}
+//@highlight \hlendcode{}
+