adjusting travis

.travis.yml

@@ -6,7 +6,7 @@ env:
 before_install:
   - until sudo add-apt-repository -y ppa:saiarcot895/chromium-beta; do echo retry; done
   - until sudo add-apt-repository --yes ppa:kalakris/cmake; do echo retry; done
-  - until sudo apt-get -qq update; do echo retry; done 
+  - until sudo apt-get -qq update; do echo retry; done
   - until sudo apt-get install cmake; do echo retry; done
   - OPAM_DEPENDS="ocamlgraph ocamlfind"
   - chmod +x ./.ocaml-config.sh
@@ -24,7 +24,7 @@ install:
   - ls $LZ
   - export Z3="$TRAVIS_BUILD_DIR/../z3"
   - mkdir -p $Z3
-  - wget --output-document=zustre.tar.gz  https://www.dropbox.com/s/wqvh31085s49ia4/zustre.tar.gz?dl=1;
+  - wget --output-document=zustre.tar.gz https://www.dropbox.com/s/9cvef743630rten/zustre.tar.gz?dl=1;
   - tar xvf zustre.tar.gz --strip-components=1 -C $Z3;
   - ls $LZ
   - ls $Z3
@@ -43,12 +43,12 @@ script:
   - cd build
   - /usr/bin/cmake -DLUSTREC_EXECUTABLE=/home/travis/build/coco-team/lustrec/bin/lustrec -DZ3_ROOT=$Z3 -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=run -DCMAKE_PROGRAM_PATH=/usr/bin  ../;
   - /usr/bin/cmake --build .
-  - /usr/bin/cmake --build . --target install 
+  - /usr/bin/cmake --build . --target install
   - cd ..
   - ls build/run/bin
   - ./build/run/bin/zustre -h
   -  python src/reg_test.py ./build/run/bin/zustre
-  
+
 
 
 

autom4te.cache/requests

@@ -14,63 +14,63 @@
                         'configure.ac'
                       ],
                       {
-                        'AM_AUTOMAKE_VERSION' => 1,
-                        '_AM_MAKEFILE_INCLUDE' => 1,
-                        'm4_pattern_forbid' => 1,
-                        'AC_LIBSOURCE' => 1,
+                        'm4_pattern_allow' => 1,
+                        'AC_CANONICAL_SYSTEM' => 1,
                         'AM_PROG_F77_C_O' => 1,
-                        'AC_CANONICAL_HOST' => 1,
-                        'AC_CONFIG_HEADERS' => 1,
                         'AC_FC_PP_DEFINE' => 1,
-                        'AC_SUBST' => 1,
+                        'AM_INIT_AUTOMAKE' => 1,
+                        'LT_CONFIG_LTDL_DIR' => 1,
+                        'AC_LIBSOURCE' => 1,
+                        'AM_POT_TOOLS' => 1,
+                        'AC_CONFIG_LINKS' => 1,
+                        'LT_INIT' => 1,
+                        '_AM_COND_IF' => 1,
+                        'AM_MAKEFILE_INCLUDE' => 1,
                         '_AM_COND_ELSE' => 1,
+                        'AC_CONFIG_SUBDIRS' => 1,
+                        'AC_SUBST' => 1,
+                        'AC_DEFINE_TRACE_LITERAL' => 1,
+                        'm4_include' => 1,
+                        'm4_pattern_forbid' => 1,
                         'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
-                        'LT_INIT' => 1,
+                        '_AM_MAKEFILE_INCLUDE' => 1,
+                        'AM_PROG_AR' => 1,
+                        'LT_SUPPORTED_TAG' => 1,
+                        'AC_CONFIG_AUX_DIR' => 1,
+                        'AC_CONFIG_LIBOBJ_DIR' => 1,
                         'AC_PROG_LIBTOOL' => 1,
-                        'm4_include' => 1,
-                        'AM_PROG_CC_C_O' => 1,
-                        '_LT_AC_TAGCONFIG' => 1,
-                        'AC_CONFIG_FILES' => 1,
+                        'AC_FC_PP_SRCEXT' => 1,
                         'AC_CANONICAL_BUILD' => 1,
-                        'AM_MAINTAINER_MODE' => 1,
-                        'AC_FC_FREEFORM' => 1,
-                        'm4_pattern_allow' => 1,
-                        'AM_PROG_MOC' => 1,
-                        'AC_CONFIG_LINKS' => 1,
-                        '_AM_COND_IF' => 1,
-                        'AM_NLS' => 1,
-                        'AC_INIT' => 1,
-                        'AC_FC_SRCEXT' => 1,
+                        'AM_SILENT_RULES' => 1,
+                        'AC_CONFIG_FILES' => 1,
                         '_m4_warn' => 1,
-                        'AM_PATH_GUILE' => 1,
-                        'AC_DEFINE_TRACE_LITERAL' => 1,
-                        'AM_MAKEFILE_INCLUDE' => 1,
-                        'sinclude' => 1,
-                        'LT_CONFIG_LTDL_DIR' => 1,
-                        'AM_INIT_AUTOMAKE' => 1,
-                        'AM_GNU_GETTEXT' => 1,
-                        'AC_REQUIRE_AUX_FILE' => 1,
-                        'AC_CANONICAL_SYSTEM' => 1,
-                        'AM_PROG_CXX_C_O' => 1,
+                        'AC_FC_SRCEXT' => 1,
+                        'AC_INIT' => 1,
+                        'AC_CANONICAL_TARGET' => 1,
+                        'AC_CANONICAL_HOST' => 1,
+                        'AC_FC_FREEFORM' => 1,
                         'AH_OUTPUT' => 1,
-                        'include' => 1,
-                        'AM_ENABLE_MULTILIB' => 1,
+                        '_AM_SUBST_NOTMAKE' => 1,
                         'm4_sinclude' => 1,
-                        'AM_XGETTEXT_OPTION' => 1,
+                        'AM_MAINTAINER_MODE' => 1,
+                        'sinclude' => 1,
                         '_AM_COND_ENDIF' => 1,
-                        'AM_PROG_FC_C_O' => 1,
-                        'AC_CONFIG_AUX_DIR' => 1,
-                        'AM_POT_TOOLS' => 1,
-                        'AC_CONFIG_LIBOBJ_DIR' => 1,
+                        'AM_XGETTEXT_OPTION' => 1,
                         'AC_SUBST_TRACE' => 1,
-                        'AC_CANONICAL_TARGET' => 1,
-                        'AC_CONFIG_SUBDIRS' => 1,
-                        'AM_PROG_AR' => 1,
-                        'LT_SUPPORTED_TAG' => 1,
+                        '_LT_AC_TAGCONFIG' => 1,
+                        'AM_PROG_CXX_C_O' => 1,
+                        'include' => 1,
+                        'AM_GNU_GETTEXT' => 1,
+                        'AC_CONFIG_HEADERS' => 1,
+                        'AM_NLS' => 1,
                         'AM_CONDITIONAL' => 1,
-                        '_AM_SUBST_NOTMAKE' => 1,
-                        'AM_SILENT_RULES' => 1,
-                        'AC_FC_PP_SRCEXT' => 1
+                        'AM_PROG_FC_C_O' => 1,
+                        'AC_REQUIRE_AUX_FILE' => 1,
+                        'AM_PROG_MOC' => 1,
+                        'AM_ENABLE_MULTILIB' => 1,
+                        'AM_AUTOMAKE_VERSION' => 1,
+                        'AM_PROG_CC_C_O' => 1,
+                        'AM_PATH_GUILE' => 1
                       }
                     ], 'Autom4te::Request' )
            );

src/Makefile

-
-OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -no-links 
+OCAMLBUILD=/opt/local/bin/ocamlbuild -classic-display -use-ocamlfind -no-links 
 
 prefix=/usr/local
 exec_prefix=${prefix}

src/backends/Horn/horn_backend_printers.ml

@@ -49,37 +49,41 @@ let rec pp_horn_const fmt c =
 let rec get_type_cst c =
   match c with
   | Const_int(n) -> new_ty Tint
-  | Const_real(x) -> new_ty Treal
-  | Const_float(f) -> new_ty Treal
+  | Const_real _ -> new_ty Treal
+  (* | Const_float _ -> new_ty Treal *)
   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l)))
   | Const_tag(tag) -> new_ty Tbool
   | Const_string(str) ->  assert false(* used only for annotations *)
   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l))
 
-let rec get_type v = 
+let rec get_type v =
   match v with
-  | Cst c -> get_type_cst c             
+  | Cst c -> get_type_cst c
   | Access(tab, index) -> begin
-                           let rec remove_link ltype = match (dynamic_type ltype).tdesc with 
-                             | Tlink t -> t
-                             | _ -> ltype
-                           in
-                            match (dynamic_type (remove_link (get_type tab))).tdesc with
-                            | Tarray(size, t) -> remove_link t
-                            | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
-                            | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
-                            | _ -> Format.eprintf "Type of access is not an array "; assert false
+      let rec remove_link ltype =
+        match (dynamic_type ltype).tdesc with
+        | Tlink t -> t
+        | _ -> ltype
+      in
+      match (dynamic_type (remove_link (get_type tab))).tdesc with
+      | Tarray(size, t) -> remove_link t
+      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
+      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
+      | _ -> Format.eprintf "Type of access is not an array "; assert false
                           end
   | Power(v, n) -> assert false
   | LocalVar v -> v.var_type
   | StateVar v -> v.var_type
   | Fun(n, vl) -> begin match n with
-                  | "+" 
-                  | "-" 
+                  | "+"
+                  | "-"
                   | "*" -> get_type (List.hd vl)
                   | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
                   end
-  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l)))
+  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
+                                 (Location.dummy_loc)
+                                 (List.length l),
+                               get_type (List.hd l)))
   | _ -> assert false
 
 
@@ -116,7 +120,7 @@ let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
                               let rec print tab x =
                                 match tab with
                                 | [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*)
-                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")" 
+                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")"
                               in
                               print initlist 0
     | Access(tab,index)      -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")"
@@ -458,7 +462,7 @@ let print_machine machines fmt m =
 
 
 let mk_flags arity =
- let b_range =
+  let b_range =
    let rec range i j =
      if i > arity then [] else i :: (range (i+1) j) in
    range 2 arity;

src/main_lustre_compiler.ml

@@ -459,7 +459,7 @@ let _ =
     Printexc.record_backtrace true;
     Printf.eprintf "\nParsing\n";
     Arg.parse Options.options anonymous usage;
-    Printf.eprintf "\nDest=%s\n" !Options.dest_file
+    Printf.eprintf "\nDest=%s\n" !Options.dest_file;
 
 
     let options = Options.options @