1 |
719ae9fd
|
Lélio Brun
|
(env
|
2 |
|
|
(dev
|
3 |
|
|
(flags (:standard -warn-error -A))))
|
4 |
|
|
|
5 |
|
|
(include_subdirs unqualified)
|
6 |
|
|
|
7 |
|
|
(library
|
8 |
|
|
(name lustrec_interface)
|
9 |
|
|
(package lustrec)
|
10 |
|
|
(modules
|
11 |
|
|
lustre_types
|
12 |
|
|
utils
|
13 |
|
|
lustre_utils
|
14 |
|
|
location
|
15 |
|
|
dimension
|
16 |
|
|
env
|
17 |
|
|
real
|
18 |
|
|
types
|
19 |
|
|
options
|
20 |
|
|
version
|
21 |
|
|
clocks
|
22 |
|
|
delay
|
23 |
|
|
machine_code_types
|
24 |
7ee5f69e
|
Lélio Brun
|
spec_types
|
25 |
75c459f4
|
Lélio Brun
|
spec_common
|
26 |
719ae9fd
|
Lélio Brun
|
scheduling_type
|
27 |
|
|
log
|
28 |
|
|
printers
|
29 |
|
|
corelang
|
30 |
|
|
basic_library
|
31 |
|
|
type_predef
|
32 |
|
|
clock_predef
|
33 |
|
|
delay_predef
|
34 |
|
|
error
|
35 |
|
|
global
|
36 |
|
|
annotations
|
37 |
|
|
machine_code_common
|
38 |
|
|
arrow
|
39 |
|
|
options_management
|
40 |
|
|
stateless
|
41 |
|
|
c_backend_common
|
42 |
|
|
typing
|
43 |
|
|
ocaml_utils
|
44 |
|
|
backends
|
45 |
|
|
lustrec_mpfr
|
46 |
|
|
normalization
|
47 |
|
|
machine_types
|
48 |
|
|
splitting
|
49 |
|
|
compiler_common
|
50 |
90e83deb
|
Lélio Brun
|
parse parser_lustre parser_lustre_table parser_lustre_messages
|
51 |
|
|
lexer_lustre lexerLustreSpec
|
52 |
719ae9fd
|
Lélio Brun
|
automata
|
53 |
|
|
clock_calculus
|
54 |
|
|
)
|
55 |
|
|
(wrapped false)
|
56 |
90e83deb
|
Lélio Brun
|
(libraries sites ocamlgraph zarith unix str menhirLib))
|
57 |
719ae9fd
|
Lélio Brun
|
|
58 |
|
|
(library
|
59 |
|
|
(name plugin_register)
|
60 |
|
|
(package lustrec)
|
61 |
|
|
(wrapped false)
|
62 |
|
|
(modules pluginList pluginType)
|
63 |
|
|
(libraries lustrec_interface))
|
64 |
|
|
|
65 |
|
|
(generate_sites_module
|
66 |
|
|
(module sites)
|
67 |
57c96fb7
|
Lélio Brun
|
; (sites lustrec)
|
68 |
|
|
(plugins
|
69 |
|
|
(lustrec plugins)
|
70 |
|
|
(lustrec verifiers)))
|
71 |
719ae9fd
|
Lélio Brun
|
|
72 |
|
|
(library
|
73 |
|
|
(name sites)
|
74 |
|
|
(package lustrec)
|
75 |
|
|
(modules sites)
|
76 |
|
|
(libraries dune-site dune-site.plugins))
|
77 |
|
|
|
78 |
|
|
(library
|
79 |
|
|
(name lustrec_lib)
|
80 |
|
|
(package lustrec)
|
81 |
|
|
(modules
|
82 |
|
|
lusic
|
83 |
|
|
c_backend_header c_backend_spec c_backend_makefile
|
84 |
efcc8d7f
|
Lélio Brun
|
c_backend_mauve c_backend_src
|
85 |
719ae9fd
|
Lélio Brun
|
ada_backend ada_printer ada_backend_common ada_backend_ads ada_backend_adb
|
86 |
|
|
ada_backend_wrapper
|
87 |
|
|
horn_backend horn_backend_common horn_backend_printers
|
88 |
|
|
Horn_backend_collecting_sem horn_backend_traces
|
89 |
|
|
EMF_backend EMF_common EMF_library_calls
|
90 |
|
|
misc_lustre_function misc_printer
|
91 |
|
|
machine_code
|
92 |
|
|
causality
|
93 |
|
|
scheduling
|
94 |
|
|
liveness
|
95 |
|
|
compiler_stages
|
96 |
|
|
modules
|
97 |
|
|
sortProg
|
98 |
|
|
inliner
|
99 |
|
|
access
|
100 |
|
|
algebraicLoop
|
101 |
|
|
optimize_prog
|
102 |
|
|
optimize_machine
|
103 |
|
|
spec
|
104 |
|
|
c_backend c_backend_main
|
105 |
|
|
plugins
|
106 |
|
|
)
|
107 |
|
|
(wrapped false)
|
108 |
|
|
(libraries sites lustrec_interface plugin_register))
|
109 |
|
|
|
110 |
|
|
(executable
|
111 |
|
|
(name main_lustre_compiler)
|
112 |
|
|
(public_name lustrec)
|
113 |
|
|
(modules main_lustre_compiler)
|
114 |
|
|
(package lustrec)
|
115 |
|
|
(libraries lustrec_lib lustrec.scopes))
|
116 |
|
|
|
117 |
|
|
(executable
|
118 |
|
|
(name main_lustre_testgen)
|
119 |
|
|
(public_name lustret)
|
120 |
|
|
(modules main_lustre_testgen mutation mmap pathConditions)
|
121 |
|
|
(libraries lustrec_lib))
|
122 |
|
|
|
123 |
|
|
(library
|
124 |
|
|
(name verifier_register)
|
125 |
|
|
(package lustrec)
|
126 |
|
|
(wrapped false)
|
127 |
|
|
(modules verifierList verifierType)
|
128 |
|
|
(libraries lustrec_interface))
|
129 |
|
|
|
130 |
|
|
(executable
|
131 |
|
|
(name main_lustre_verifier)
|
132 |
|
|
(public_name lustrev)
|
133 |
|
|
(modules main_lustre_verifier verifiers)
|
134 |
|
|
(libraries lustrec_lib verifier_register lustrec.scopes))
|
135 |
ca7e8027
|
Lélio Brun
|
|
136 |
|
|
(executable
|
137 |
|
|
(name main_lustre_importer)
|
138 |
|
|
(public_name lustrei)
|
139 |
|
|
(modules main_lustre_importer vhdl_deriving_yojson vhdl_json_lib)
|
140 |
|
|
(libraries yojson ppx_deriving_yojson.runtime)
|
141 |
|
|
(preprocess (pps ppx_deriving_yojson)))
|
142 |
|
|
|
143 |
|
|
(library
|
144 |
|
|
(name tools_lib)
|
145 |
|
|
(package lustrec)
|
146 |
|
|
(wrapped false)
|
147 |
|
|
(modules basetypes datatype activeStates)
|
148 |
|
|
(libraries lustrec_lib))
|
149 |
|
|
|
150 |
|
|
(executable
|
151 |
|
|
(name sf_sem)
|
152 |
|
|
(public_name lustresf)
|
153 |
|
|
(modules
|
154 |
|
|
sf_sem
|
155 |
|
|
model_simple
|
156 |
|
|
model_stopwatch
|
157 |
|
|
CPS_ccode_generator
|
158 |
|
|
CPS_transformer
|
159 |
|
|
CPS_interpreter
|
160 |
|
|
CPS_lustre_generator
|
161 |
|
|
CPS
|
162 |
|
|
theta
|
163 |
|
|
memo)
|
164 |
|
|
(libraries tools_lib))
|
165 |
|
|
|
166 |
57c96fb7
|
Lélio Brun
|
|
167 |
|
|
|
168 |
ca7e8027
|
Lélio Brun
|
; (executable
|
169 |
|
|
; (name main_parse_json_file)
|
170 |
|
|
; (public_name json-parser)
|
171 |
|
|
; (modules main_parse_json_file json_parser)
|
172 |
|
|
; (libraries tools_lib cmdliner))
|
173 |
|
|
|
174 |
|
|
; (executable
|
175 |
|
|
; (name test_json_parser_variables)
|
176 |
|
|
; (modules test_json_parser_variables json_parser)
|
177 |
|
|
; (libraries tools_lib))
|