Commits

Zachary Anderson committed 7037352

Added and fixed a few tests

Comments (0)

Files changed (11)

ciltut-lib/src/CMakeLists.txt

 
 add_library(ciltut-static ${SHELTER_SRCS})
 set_target_properties(ciltut-static PROPERTIES
-  COMPILE_FLAGS -O2
+  COMPILE_FLAGS "-O2 -ggdb"
 )
 set_target_properties(ciltut-static
   PROPERTIES OUTPUT_NAME ciltut
 
 add_library(ciltut-shared SHARED ${SHELTER_SRCS})
 set_target_properties(ciltut-shared PROPERTIES
-  COMPILE_FLAGS -O2
+  COMPILE_FLAGS "-O2 -ggdb"
 )
 set_target_properties(ciltut-shared
   PROPERTIES OUTPUT_NAME ciltut

ciltut-lib/src/tut10.c

 
 
 pthread_key_t CS_key;
+static void init_CS()
+{
+  struct cache_stack *CS = calloc(1, sizeof(*CS));
+  pthread_setspecific(CS_key, CS);
+}
+
 CONSTRUCTOR static void init_CS_key()
 {
-  struct cache_stack *CS = calloc(1, sizeof(*CS));
   pthread_key_create(&CS_key, &free);
-  pthread_setspecific(CS_key, CS);
+	init_CS();
 }
+
 static struct cache_stack *get_CS()
 {
   return (struct cache_stack *)pthread_getspecific(CS_key);
 
   free(c);
 
-  init_CS_key();
+  init_CS();
   perf_init(gettid());
   res = fn(a);
   perf_deinit();
   visitCilFile vis f
 
 
-
-
 let invariantAttrStr = "invariant"
 let postAttrStr      = "post"
 let preAttrStr       = "pre"
+let tut11_attrs = [invariantAttrStr; postAttrStr; preAttrStr;]
 
 
 
     validateWhyCtxt wc vc
 
 
+class attrEraserVisitor = object(self)
+  inherit nopCilVisitor
+
+  method vattr (a : attribute) =
+    match a with
+    | Attr(s,_) when L.mem s tut11_attrs -> ChangeTo []
+    | _ -> DoChildren
+
+end
+
+let eraseAttrs (f : file) : unit =
+  let vis = new attrEraserVisitor in
+  visitCilFile vis f
+
+
+
 
 let tut11 (f : file) : unit =
   let wc = initWhyCtxt (!Ciltutoptions.prover) in
-  iterGlobals f (onlyFunctions (processFunction wc))
+  iterGlobals f (onlyFunctions (processFunction wc));
+	eraseAttrs f
 
 
 ELSE
 
   method vexpr (e : exp) =
     match e with
-    | CastE(t, e) ->
+    | CastE(t, e) when not(isConstant e) ->
       let tcres = colorTypesCompat t (typeOf e) in
       warning_for_tcres tcres;
       DoChildren
   ignore(visitCilFunction vis fd)
 
 
+class colorEraserVisitor = object(self)
+  inherit nopCilVisitor
+
+  method vattr (a : attribute) =
+    match a with
+    | Attr(s,_) when L.mem s color_strings -> ChangeTo []
+    | _ -> DoChildren
+
+end
+
+let eraseColors (f : file) : unit =
+  let vis = new colorEraserVisitor in
+  visitCilFile vis f
+
+
 
 let tut7 (f : file) : unit =
-  iterGlobals f (onlyFunctions checkColorTypes)
+  iterGlobals f (onlyFunctions checkColorTypes);
+	eraseColors f
 
 
 
 
 end
 
+let checkColorTypes (c : ctxt) (fd : fundec) (loc : location) : unit =
+  let c = context_for_locals c fd in
+  let vis = new colorCheckVisitor c in
+  ignore(visitCilFunction vis fd)
+
 
 class colorEraserVisitor = object(self)
   inherit nopCilVisitor
 
 end
 
-let checkColorTypes (c : ctxt) (fd : fundec) (loc : location) : unit =
-  let c = context_for_locals c fd in
-  let vis = new colorCheckVisitor c in
-  ignore(visitCilFunction vis fd)
-
 let eraseColors (f : file) : unit =
   let vis = new colorEraserVisitor in
   visitCilFile vis f
 
+
 let tut8_init (f : file) : unit =
   initColorFunctions f
 
 #include <stdlib.h>
 #include <ciltut.h>
 
-#define DATA_SIZE 500000000
+#define DATA_SIZE 50000000
 #define TIMES 5
 
 struct array {
 \noindent
 \ttfamily
-\hlstd{}\section{\texttt{tut11.c}}\hlstd{}\hltscom{This C source file contains an example function that we \hlstd{}will use to demonstrate the features developed in\hlstd{}\texttt{tut11.ml}. In particular we will verify that a function \hlstd{}will successfully initialize an integer array to contain the \hlstd{}number 4 at each entry.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
+\hlstd{}\section{\texttt{test/tut11.c}}\hlstd{}\hltscom{This C source file contains an example function that we \hlstd{}will use to demonstrate the features developed in\hlstd{}\texttt{tut11.ml}. In particular we will verify that a function \hlstd{}will successfully initialize an integer array to contain the \hlstd{}number 4 at each entry.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
 \hldir{\#include\ $<$ciltut.h$>$\ }\hlslc{//\ For\ the\ pre,\ post\ and\ invariant\ annotations.}\hspace*{\fill}\\
 \hldir{}\hlstd{}\hlendcode{}\hlstd{}\hltscom{The function \texttt{arr\_init} loops over the given \hlstd{}array setting each element to 4. The precondition to the function \hlstd{}states that the parameter \texttt{n} must be positive. The \hlstd{}postcondition states that each element of the array is 4. The\hlstd{}loop invariant states that the loop index stays in bounds, and\hlstd{}that the array up to the value of the loop index is initialized \hlstd{}to be 4.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
 \hlkwb{void\ }\hlstd{}\hlsym{(}\hlstd{}\hlkwd{pre}\hlstd{}\hlsym{(}\hlstd{n\ }\hlsym{$>$\ }\hlstd{}\hlnum{0}\hlstd{}\hlsym{)}\hspace*{\fill}\\
+
+
+
+
+
+
+
+
+#include <ciltut.h>
+
+int blue b;
+
+int main()
+{
+  int green g = AddColor(green, 5);
+  b = g;
+  return 0;
+}
+
-#include <stdio.h>
+
+
+
+
+
+
+
+
+
+
+
+
 #include <ciltut.h>
 
 struct bar {
   return;
 }
 
+void bar(int UpperRGB(r,g,b) c, int r, int g, int b)
+{
+  return;
+}
+
 int main()
 {
   struct bar B;
   B.c = AddRGB(50,50,50,50);
 
   foo(B.c, B.r, B.g, B.b);
+  bar(B.c, 10, 10, 10);
 
   return 0;
 }
-#include <stdio.h>
+
+
+
+
+
+
 #include <ciltut.h>
 
 struct bar {
   int red * red r;
   int green g;
-  int blue b;
   int red green blue c;
 };
 
-void foo(int blue c, int r, int g, int b)
+void foo(int blue c, int r, int g)
 {
   return;
 }
 
   B.r = &r;
   B.g = 50;
-  B.b = 50;
   B.c = AddColor(blue, 50);
 
-  foo(B.c, *B.r, B.g, B.b);
+  foo(B.c, *B.r, B.g);
+  foo(B.g, r, r);
 
   return 0;
 }