Revision e057dd08
Added by Teme Kahsai over 6 years ago
| .travis.yml | ||
|---|---|---|
| 6 | 6 |
before_install: |
| 7 | 7 |
- until sudo add-apt-repository -y ppa:saiarcot895/chromium-beta; do echo retry; done |
| 8 | 8 |
- until sudo add-apt-repository --yes ppa:kalakris/cmake; do echo retry; done |
| 9 |
- until sudo apt-get -qq update; do echo retry; done
|
|
| 9 |
- until sudo apt-get -qq update; do echo retry; done |
|
| 10 | 10 |
- until sudo apt-get install cmake; do echo retry; done |
| 11 | 11 |
- OPAM_DEPENDS="ocamlgraph ocamlfind" |
| 12 | 12 |
- chmod +x ./.ocaml-config.sh |
| ... | ... | |
| 24 | 24 |
- ls $LZ |
| 25 | 25 |
- export Z3="$TRAVIS_BUILD_DIR/../z3" |
| 26 | 26 |
- mkdir -p $Z3 |
| 27 |
- wget --output-document=zustre.tar.gz https://www.dropbox.com/s/wqvh31085s49ia4/zustre.tar.gz?dl=1;
|
|
| 27 |
- wget --output-document=zustre.tar.gz https://www.dropbox.com/s/9cvef743630rten/zustre.tar.gz?dl=1;
|
|
| 28 | 28 |
- tar xvf zustre.tar.gz --strip-components=1 -C $Z3; |
| 29 | 29 |
- ls $LZ |
| 30 | 30 |
- ls $Z3 |
| ... | ... | |
| 43 | 43 |
- cd build |
| 44 | 44 |
- /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 ../; |
| 45 | 45 |
- /usr/bin/cmake --build . |
| 46 |
- /usr/bin/cmake --build . --target install
|
|
| 46 |
- /usr/bin/cmake --build . --target install |
|
| 47 | 47 |
- cd .. |
| 48 | 48 |
- ls build/run/bin |
| 49 | 49 |
- ./build/run/bin/zustre -h |
| 50 | 50 |
- python src/reg_test.py ./build/run/bin/zustre |
| 51 |
|
|
| 51 |
|
|
| 52 | 52 |
|
| 53 | 53 |
|
| 54 | 54 |
|
| autom4te.cache/requests | ||
|---|---|---|
| 14 | 14 |
'configure.ac' |
| 15 | 15 |
], |
| 16 | 16 |
{
|
| 17 |
'AM_AUTOMAKE_VERSION' => 1, |
|
| 18 |
'_AM_MAKEFILE_INCLUDE' => 1, |
|
| 19 |
'm4_pattern_forbid' => 1, |
|
| 20 |
'AC_LIBSOURCE' => 1, |
|
| 17 |
'm4_pattern_allow' => 1, |
|
| 18 |
'AC_CANONICAL_SYSTEM' => 1, |
|
| 21 | 19 |
'AM_PROG_F77_C_O' => 1, |
| 22 |
'AC_CANONICAL_HOST' => 1, |
|
| 23 |
'AC_CONFIG_HEADERS' => 1, |
|
| 24 | 20 |
'AC_FC_PP_DEFINE' => 1, |
| 25 |
'AC_SUBST' => 1, |
|
| 21 |
'AM_INIT_AUTOMAKE' => 1, |
|
| 22 |
'LT_CONFIG_LTDL_DIR' => 1, |
|
| 23 |
'AC_LIBSOURCE' => 1, |
|
| 24 |
'AM_POT_TOOLS' => 1, |
|
| 25 |
'AC_CONFIG_LINKS' => 1, |
|
| 26 |
'LT_INIT' => 1, |
|
| 27 |
'_AM_COND_IF' => 1, |
|
| 28 |
'AM_MAKEFILE_INCLUDE' => 1, |
|
| 26 | 29 |
'_AM_COND_ELSE' => 1, |
| 30 |
'AC_CONFIG_SUBDIRS' => 1, |
|
| 31 |
'AC_SUBST' => 1, |
|
| 32 |
'AC_DEFINE_TRACE_LITERAL' => 1, |
|
| 33 |
'm4_include' => 1, |
|
| 34 |
'm4_pattern_forbid' => 1, |
|
| 27 | 35 |
'AM_GNU_GETTEXT_INTL_SUBDIR' => 1, |
| 28 |
'LT_INIT' => 1, |
|
| 36 |
'_AM_MAKEFILE_INCLUDE' => 1, |
|
| 37 |
'AM_PROG_AR' => 1, |
|
| 38 |
'LT_SUPPORTED_TAG' => 1, |
|
| 39 |
'AC_CONFIG_AUX_DIR' => 1, |
|
| 40 |
'AC_CONFIG_LIBOBJ_DIR' => 1, |
|
| 29 | 41 |
'AC_PROG_LIBTOOL' => 1, |
| 30 |
'm4_include' => 1, |
|
| 31 |
'AM_PROG_CC_C_O' => 1, |
|
| 32 |
'_LT_AC_TAGCONFIG' => 1, |
|
| 33 |
'AC_CONFIG_FILES' => 1, |
|
| 42 |
'AC_FC_PP_SRCEXT' => 1, |
|
| 34 | 43 |
'AC_CANONICAL_BUILD' => 1, |
| 35 |
'AM_MAINTAINER_MODE' => 1, |
|
| 36 |
'AC_FC_FREEFORM' => 1, |
|
| 37 |
'm4_pattern_allow' => 1, |
|
| 38 |
'AM_PROG_MOC' => 1, |
|
| 39 |
'AC_CONFIG_LINKS' => 1, |
|
| 40 |
'_AM_COND_IF' => 1, |
|
| 41 |
'AM_NLS' => 1, |
|
| 42 |
'AC_INIT' => 1, |
|
| 43 |
'AC_FC_SRCEXT' => 1, |
|
| 44 |
'AM_SILENT_RULES' => 1, |
|
| 45 |
'AC_CONFIG_FILES' => 1, |
|
| 44 | 46 |
'_m4_warn' => 1, |
| 45 |
'AM_PATH_GUILE' => 1, |
|
| 46 |
'AC_DEFINE_TRACE_LITERAL' => 1, |
|
| 47 |
'AM_MAKEFILE_INCLUDE' => 1, |
|
| 48 |
'sinclude' => 1, |
|
| 49 |
'LT_CONFIG_LTDL_DIR' => 1, |
|
| 50 |
'AM_INIT_AUTOMAKE' => 1, |
|
| 51 |
'AM_GNU_GETTEXT' => 1, |
|
| 52 |
'AC_REQUIRE_AUX_FILE' => 1, |
|
| 53 |
'AC_CANONICAL_SYSTEM' => 1, |
|
| 54 |
'AM_PROG_CXX_C_O' => 1, |
|
| 47 |
'AC_FC_SRCEXT' => 1, |
|
| 48 |
'AC_INIT' => 1, |
|
| 49 |
'AC_CANONICAL_TARGET' => 1, |
|
| 50 |
'AC_CANONICAL_HOST' => 1, |
|
| 51 |
'AC_FC_FREEFORM' => 1, |
|
| 55 | 52 |
'AH_OUTPUT' => 1, |
| 56 |
'include' => 1, |
|
| 57 |
'AM_ENABLE_MULTILIB' => 1, |
|
| 53 |
'_AM_SUBST_NOTMAKE' => 1, |
|
| 58 | 54 |
'm4_sinclude' => 1, |
| 59 |
'AM_XGETTEXT_OPTION' => 1, |
|
| 55 |
'AM_MAINTAINER_MODE' => 1, |
|
| 56 |
'sinclude' => 1, |
|
| 60 | 57 |
'_AM_COND_ENDIF' => 1, |
| 61 |
'AM_PROG_FC_C_O' => 1, |
|
| 62 |
'AC_CONFIG_AUX_DIR' => 1, |
|
| 63 |
'AM_POT_TOOLS' => 1, |
|
| 64 |
'AC_CONFIG_LIBOBJ_DIR' => 1, |
|
| 58 |
'AM_XGETTEXT_OPTION' => 1, |
|
| 65 | 59 |
'AC_SUBST_TRACE' => 1, |
| 66 |
'AC_CANONICAL_TARGET' => 1, |
|
| 67 |
'AC_CONFIG_SUBDIRS' => 1, |
|
| 68 |
'AM_PROG_AR' => 1, |
|
| 69 |
'LT_SUPPORTED_TAG' => 1, |
|
| 60 |
'_LT_AC_TAGCONFIG' => 1, |
|
| 61 |
'AM_PROG_CXX_C_O' => 1, |
|
| 62 |
'include' => 1, |
|
| 63 |
'AM_GNU_GETTEXT' => 1, |
|
| 64 |
'AC_CONFIG_HEADERS' => 1, |
|
| 65 |
'AM_NLS' => 1, |
|
| 70 | 66 |
'AM_CONDITIONAL' => 1, |
| 71 |
'_AM_SUBST_NOTMAKE' => 1, |
|
| 72 |
'AM_SILENT_RULES' => 1, |
|
| 73 |
'AC_FC_PP_SRCEXT' => 1 |
|
| 67 |
'AM_PROG_FC_C_O' => 1, |
|
| 68 |
'AC_REQUIRE_AUX_FILE' => 1, |
|
| 69 |
'AM_PROG_MOC' => 1, |
|
| 70 |
'AM_ENABLE_MULTILIB' => 1, |
|
| 71 |
'AM_AUTOMAKE_VERSION' => 1, |
|
| 72 |
'AM_PROG_CC_C_O' => 1, |
|
| 73 |
'AM_PATH_GUILE' => 1 |
|
| 74 | 74 |
} |
| 75 | 75 |
], 'Autom4te::Request' ) |
| 76 | 76 |
); |
| src/Makefile | ||
|---|---|---|
| 1 |
|
|
| 2 |
OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -no-links |
|
| 1 |
OCAMLBUILD=/opt/local/bin/ocamlbuild -classic-display -use-ocamlfind -no-links |
|
| 3 | 2 |
|
| 4 | 3 |
prefix=/usr/local |
| 5 | 4 |
exec_prefix=${prefix}
|
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 49 | 49 |
let rec get_type_cst c = |
| 50 | 50 |
match c with |
| 51 | 51 |
| Const_int(n) -> new_ty Tint |
| 52 |
| Const_real(x) -> new_ty Treal
|
|
| 53 |
| Const_float(f) -> new_ty Treal
|
|
| 52 |
| Const_real _ -> new_ty Treal
|
|
| 53 |
(* | Const_float _ -> new_ty Treal *)
|
|
| 54 | 54 |
| Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l))) |
| 55 | 55 |
| Const_tag(tag) -> new_ty Tbool |
| 56 | 56 |
| Const_string(str) -> assert false(* used only for annotations *) |
| 57 | 57 |
| Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) |
| 58 | 58 |
|
| 59 |
let rec get_type v =
|
|
| 59 |
let rec get_type v = |
|
| 60 | 60 |
match v with |
| 61 |
| Cst c -> get_type_cst c
|
|
| 61 |
| Cst c -> get_type_cst c |
|
| 62 | 62 |
| Access(tab, index) -> begin |
| 63 |
let rec remove_link ltype = match (dynamic_type ltype).tdesc with |
|
| 64 |
| Tlink t -> t |
|
| 65 |
| _ -> ltype |
|
| 66 |
in |
|
| 67 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
| 68 |
| Tarray(size, t) -> remove_link t |
|
| 69 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 70 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 71 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
| 63 |
let rec remove_link ltype = |
|
| 64 |
match (dynamic_type ltype).tdesc with |
|
| 65 |
| Tlink t -> t |
|
| 66 |
| _ -> ltype |
|
| 67 |
in |
|
| 68 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
| 69 |
| Tarray(size, t) -> remove_link t |
|
| 70 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 71 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 72 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
| 72 | 73 |
end |
| 73 | 74 |
| Power(v, n) -> assert false |
| 74 | 75 |
| LocalVar v -> v.var_type |
| 75 | 76 |
| StateVar v -> v.var_type |
| 76 | 77 |
| Fun(n, vl) -> begin match n with |
| 77 |
| "+"
|
|
| 78 |
| "-"
|
|
| 78 |
| "+" |
|
| 79 |
| "-" |
|
| 79 | 80 |
| "*" -> get_type (List.hd vl) |
| 80 | 81 |
| _ -> Format.eprintf "Function undealt with : %s" n ;assert false |
| 81 | 82 |
end |
| 82 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l))) |
|
| 83 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int |
|
| 84 |
(Location.dummy_loc) |
|
| 85 |
(List.length l), |
|
| 86 |
get_type (List.hd l))) |
|
| 83 | 87 |
| _ -> assert false |
| 84 | 88 |
|
| 85 | 89 |
|
| ... | ... | |
| 116 | 120 |
let rec print tab x = |
| 117 | 121 |
match tab with |
| 118 | 122 |
| [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*) |
| 119 |
| 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 ")"
|
|
| 123 |
| 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 ")" |
|
| 120 | 124 |
in |
| 121 | 125 |
print initlist 0 |
| 122 | 126 |
| 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 | 462 |
|
| 459 | 463 |
|
| 460 | 464 |
let mk_flags arity = |
| 461 |
let b_range = |
|
| 465 |
let b_range =
|
|
| 462 | 466 |
let rec range i j = |
| 463 | 467 |
if i > arity then [] else i :: (range (i+1) j) in |
| 464 | 468 |
range 2 arity; |
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 459 | 459 |
Printexc.record_backtrace true; |
| 460 | 460 |
Printf.eprintf "\nParsing\n"; |
| 461 | 461 |
Arg.parse Options.options anonymous usage; |
| 462 |
Printf.eprintf "\nDest=%s\n" !Options.dest_file |
|
| 462 |
Printf.eprintf "\nDest=%s\n" !Options.dest_file;
|
|
| 463 | 463 |
|
| 464 | 464 |
|
| 465 | 465 |
let options = Options.options @ |
Also available in: Unified diff
adjusting travis