Commits

Zachary Anderson  committed 86324f3

Fixes for tutorials 11 and 15

  • Participants
  • Parent commits 89536f9

Comments (0)

Files changed (5)

File ciltut-lib/Makefile.dummy.in

-ifndef ARCHOS
-  ARCHOS = @ARCHOS@
-endif
-
-ifndef BUILD_DOCS
-  BUILD_DOCS = @BUILD_DOCS@
-endif
-
 ifndef BUILD_TUT11
   BUILD_TUT11 = @BUILD_TUT11@
 endif

File ciltut-lib/src/CMakeLists.txt

 	"${PROJECT_BINARY_DIR}/src/config.h"
 )
 
-if(BUILD_TUT15="true")
+message("BUILD_TUT11 = ${BUILD_TUT11}")
+message("BUILD_TUT15 = ${BUILD_TUT15}")
+
+if(${BUILD_TUT15} STREQUAL true)
 set(OCAML_COMPILE ocamlc)
 
+message("Building concolic callbacks")
+
 execute_process(
   COMMAND ocamlfind query ocamlyices
   OUTPUT_VARIABLE OCAML_YICES OUTPUT_STRIP_TRAILING_WHITESPACE
 )
 
+execute_process(
+  COMMAND ocamlfind query gmp
+  OUTPUT_VARIABLE OCAML_GMP OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+
 set(CONC_SRCS
  concolic/concolic_util.ml
  concolic/concolic_exp.ml
 add_custom_command(
   SOURCE  ${CONC_SRCS}
   COMMAND ${OCAML_COMPILE}
-  ARGS    -custom -output-obj -o concolic_callbacks.o -I concolic/ -I ${OCAML_YICES} -I +gmp gmp.cma nums.cma ocamlyices.cma ${CONC_SRCS}
+  ARGS    -custom -output-obj -o concolic_callbacks.o -I concolic/ -I ${OCAML_YICES} -I ${OCAML_GMP} gmp.cma nums.cma ocamlyices.cma ${CONC_SRCS}
   TARGET  concolic_callbacks
   OUTPUTS concolic_callbacks.o
   DEPENDS ${CONC_SRCS}

File lib/Ciltut.pm

         print STDERR "ciltutcc: no input files\n";
         return 0;
     } else {
-        unshift @libs, @{$self->{CILTUTLIBS}}, "-ldl", "-lrt";
+        unshift @libs, @{$self->{CILTUTLIBS}};
         if ($self->{TUT15} == 1) {
             my $ocy = `ocamlfind query ocamlyices`;
             chomp($ocy);
                            "-lm", "-lcurses", "-L$ocy" , "-locamlyices",
                            "-lstdc++", "/usr/local/lib/libyices.a";
         }
+        push @libs, "-ldl", "-lrt";
         return $self->SUPER::link_after_cil(\@srcs, $dest, $ppargs,
                                             \@cargs, \@libs);
     }

File src/ciltutoptions.ml

 let num_tuts = 16
 let enable_tut : bool ref array = Array.init num_tuts (fun i -> ref false)
 
-let prover : string ref = ref "alt-ergo"
+let prover : string ref = ref "Alt-Ergo"
+let prover_version : string ref = ref "0.94"
 let tut13out : string ref = ref "callgraph.dot"
 
 let options_ref = ref []
   
   ("--prover",
    Arg.Set_string prover,
-   "The prover that Why3 should use in Tut11 [default: alt-ergo]");
+   "The prover that Why3 should use in Tut11 [default: Alt-Ergo]");
+  ("--prover-version",
+   Arg.Set_string prover_version,
+   "The version for the prover that Why3 should use in Tut11 [default: 0.94]");
+
 
   
   ("--tut13-out",

File src/tut11.ml

   }
 
 
-let initWhyCtxt (p : string) : wctxt = 
+let initWhyCtxt (p : string) (pv : string) : wctxt = 
 
   let config  = Wc.read_config None in
   let main    = Wc.get_main config in
   Wc.load_plugins main;
   let provers = Wc.get_provers config in
+  Wc.Mprover.iter
+    (fun k a ->
+      Em.warn "%s %s (%s)" k.Wc.prover_name k.Wc.prover_version k.Wc.prover_altern
+    ) provers;
+  let prover_spec = {Wc.prover_name =p; Wc.prover_version=pv; Wc.prover_altern=""} in
   let prover =
-    
-    try Wc.prover_by_id config p
+    try Wc.Mprover.find prover_spec provers
     with Not_found -> Em.s (Em.error "Prover %s not found." p)
   in
   let env = E.create_env (W.Whyconf.loadpath main) in
 
 
 let tut11 (f : file) : unit =
-  let wc = initWhyCtxt (!Ciltutoptions.prover) in
+  let wc = initWhyCtxt (!Ciltutoptions.prover) (!Ciltutoptions.prover_version) in
   iterGlobals f (onlyFunctions (processFunction wc));
 	eraseAttrs f