Project

General

Profile

Revision e057dd08

View differences:

.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