Project

General

Profile

« Previous | Next » 

Revision 57c96fb7

Added by LĂ©lio Brun 11 months ago

setup tests for dune

View differences:

.gitmodules
1
[submodule "tests"]
2
	path = tests
3
	url = https://cavale.enseeiht.fr/git/lustrec-tests
dune
1
; too bad dune does not support glob in install stanza
2
; (see https://discuss.ocaml.org/t/installing-many-files-with-dune/4143)
3
; TODO: open an issue?
4

  
5
(install
6
 (section (site (lustrec include_)))
7
 (files
8
   include/conv.c
9
   include/mpfr_lustre.c
10
   include/simulink_math_fcn.c
11
   include/arrow.c
12
   include/arrow.h
13
   include/arrow.cpp
14
   include/arrow.hpp
15
   include/io_frontend.c
16
   include/io_frontend.h
17
   include/io_frontend.hpp
18
   include/lustrec_math.smt2
19
   include/mpfr_lustre.lusi
20
   include/mpfr_lustre.lusic
21
   include/simulink_math_fcn.lusi
22
   include/simulink_math_fcn.lusic
23
   include/conv.lusi
24
   include/conv.lusic
25
   include/lustrec_math.lusi
26
   include/lustrec_math.lusic
27
   include/StdIn.java))
28

  
29
(install
30
 (section (site (lustrec testgen)))
31
 (files
32
   share/FindLustre.cmake
33
   share/helpful_functions.cmake))
34

  
35
(rule
36
 (alias runtest)
37
 (deps (source_tree tests/regression_tests))
38
 (action (chdir tests/regression_tests
39
          (progn
40
           (run cmake "-DSUBPROJ=\"unstable\"" "-DLUSTRE_INCLUDE_DIR=%{project_root}/include" .)
41
           (run ctest -D Experimental -R "COMPIL_LUS|MAKE|BIN|DIFF" -E LUSTRET --progress)))))
dune-project
18 18
 (name lustrec)
19 19
 (sites
20 20
  (lib plugins)
21
  (lib verifiers))
21
  (lib verifiers)
22
  (lib include_)
23
  (share testgen))
22 24
 (synopsis "A Lustre compiler toolset")
23 25
 (description
24 26
   "lustrec is structured around the modular compilation scheme proposed by \
include/dune
1
; too bad we have to repeat the same rule three times...
2
; The make-like behavior if still unsupported by dune
3
; (see https://discuss.ocaml.org/t/dune-copy-multiple-dependencies-to-build-directory-in-rule-stanza/4144/5)
4

  
5
(rule
6
 (target conv.lusic)
7
 (action (run lustrec -verbose 0 -I . -d . %{dep:conv.lusi}))
8
 (alias install))
9

  
10
(rule
11
 (target simulink_math_fcn.lusic)
12
 (action (run lustrec -verbose 0 -I . -d . %{dep:simulink_math_fcn.lusi}))
13
 (alias install))
14

  
15
(rule
16
 (target lustrec_math.lusic)
17
 (action (run lustrec -verbose 0 -I . -d . %{dep:lustrec_math.lusi}))
18
 (alias install))
19

  
20
(rule
21
 (target mpfr_lustre.lusic)
22
 (action (run lustrec -verbose 0 -mpfr 1 -d . %{dep:mpfr_lustre.lusi}))
23
 (alias install))
share/FindLustre.cmake
1
# - Find Lustre compiler
2
# Find the Lustre synchronous language compiler with associated includes path.
3
# See https://cavale.enseeiht.fr/redmine/projects/lustrec
4
# This module defines
5
#  LUSTRE_COMPILER, the lustre compiler
6
#  LUSTRE_COMPILER_VERSION, the version of the lustre compiler
7
#  LUSTRE_INCLUDE_DIR, where to find dword.h, etc.
8
#  LUSTRE_FOUND, If false, Lustre was not found.
9
# On can set LUSTRE_PATH_HINT before using find_package(Lustre) and the
10
# module with use the PATH as a hint to find lustrec.
11
#
12
# The hint can be given on the command line too:
13
#   cmake -DLUSTRE_PATH_HINT=/DATA/ERIC/Lustre/lustre-x.y /path/to/source
14
#
15
# The module defines some functions:
16
#   Lustre_Compile([NODE <Lustre Main Node>]
17
#                  LUS_FILES <Lustre files>
18
#                  [USER_C_FILES <C files>]
19
#                  [VERBOSE <level>]
20
#                  [LUSI]
21
#                  LIBNAME <libraryName>)
22
#
23
# When used the Lustre_Compile macro define the variable
24
# LUSTRE_GENERATED_C_FILES_<libraryName> in the parent scope
25
# so that the caller can get (if needed) the list of Lustre generated files.
26
# The VERBOSE level is a numeric value passed directly to the -verbose
27
# command line option of the lustre compiler
28
#
29
include("helpful_functions.cmake")
30

  
31
if(LUSTRE_PATH_HINT)
32
  message(STATUS "FindLustre: using PATH HINT: ${LUSTRE_PATH_HINT}")
33
else()
34
  set(LUSTRE_PATH_HINT)
35
endif()
36

  
37
#One can add his/her own builtin PATH.
38
#FILE(TO_CMAKE_PATH "/DATA/ERIC/Lustre/lustre-x.y" MYPATH)
39
#list(APPEND LUSTRE_PATH_HINT ${MYPATH})
40

  
41
# FIND_PROGRAM twice using NO_DEFAULT_PATH on first shot
42
find_program(LUSTRE_COMPILER
43
  NAMES lustrec
44
  PATHS ${LUSTRE_PATH_HINT}
45
  PATH_SUFFIXES bin
46
  NO_DEFAULT_PATH
47
  DOC "Path to the Lustre compiler command 'lustrec'")
48

  
49
find_program(LUSTRE_COMPILER
50
  NAMES lustrec
51
  PATHS ${LUSTRE_PATH_HINT}
52
  PATH_SUFFIXES bin
53
  DOC "Path to the Lustre compiler command 'lustrec'")
54

  
55
if(LUSTRE_COMPILER)
56
    # get the path where the lustre compiler was found
57
    get_filename_component(LUSTRE_PATH ${LUSTRE_COMPILER} PATH)
58
    # remove bin
59
    get_filename_component(LUSTRE_PATH ${LUSTRE_PATH} PATH)
60
    # add path to LUSTRE_PATH_HINT
61
    list(APPEND LUSTRE_PATH_HINT ${LUSTRE_PATH})
62
    execute_process(COMMAND ${LUSTRE_COMPILER} -version
63
        OUTPUT_VARIABLE LUSTRE_COMPILER_VERSION
64
        OUTPUT_STRIP_TRAILING_WHITESPACE)
65
    message(STATUS "Lustre compiler version is : ${LUSTRE_COMPILER_VERSION}")
66
endif(LUSTRE_COMPILER)
67

  
68
find_path(LUSTRE_INCLUDE_DIR
69
          NAMES arrow.h
70
          PATHS ${LUSTRE_PATH_HINT}
71
          PATH_SUFFIXES include/lustrec
72
          DOC "The Lustre include headers")
73

  
74
# Macros used to compile a lustre library
75
include(CMakeParseArguments)
76
function(Lustre_Compile)
77
  set(options LUSI)
78
  set(oneValueArgs NODE LIBNAME VERBOSE)
79
  set(multiValueArgs LUS_FILES USER_C_FILES)
80
  cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
81

  
82
  if(LUS_LUSI)
83
    set(LUSTRE_LUSI_OPT "-lusi")
84
  endif()
85

  
86
  if (NOT LUS_LIBNAME)
87
    message(FATAL_ERROR "You should specify LIBNAME for each Lustre_Compile call.")
88
  endif()
89

  
90
  if(LUS_NODE)
91
    set(LUSTRE_NODE_OPT "-node;${LUS_NODE}")
92
    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}/${LUS_NODE}")
93
  else()
94
    set(LUSTRE_NODE_OPT "")
95
    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}")
96
  endif()
97

  
98
  if (LUS_VERBOSE)
99
    set(LUSTRE_VERBOSE_OPT "-verbose;${LUS_VERBOSE}")
100
  else()
101
    # the default is to be quiet.
102
    set(LUSTRE_VERBOSE_OPT "-verbose;0")
103
  endif()
104

  
105
  file(MAKE_DIRECTORY ${LUSTRE_OUTPUT_DIR})
106
  set(GLOBAL_LUSTRE_GENERATED_C_FILES "")
107
  set(GLOBAL_LUSTRE_DEP_C_FILES "")
108
  # create list of generated C files in parent scope
109
  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "" PARENT_SCOPE)
110
  foreach(LFILE IN LISTS LUS_LUS_FILES)
111
    get_lustre_name_ext(${LFILE} L E)
112
    
113
    if ("${E}" STREQUAL "lus")
114
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h ${LUSTRE_OUTPUT_DIR}/${L}.c ${LUSTRE_OUTPUT_DIR}/${L}_alloc.h)
115
      set(LUSTRE_DEP_FILES "")
116
      if(LUS_NODE)
117
         list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}_main.c)
118
         list(APPEND LUSTRE_DEP_FILES ${LUSTRE_INCLUDE_DIR}/io_frontend.c)
119
      endif()
120
    elseif("${E}" STREQUAL "lusi")
121
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h)
122
    endif()
123
    list(APPEND GLOBAL_LUSTRE_GENERATED_C_FILES ${LUSTRE_GENERATED_FILES})
124
    list(APPEND GLOBAL_LUSTRE_DEP_FILES ${LUSTRE_DEP_FILES}) # todo: add if not already in the list
125
    set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic)
126
    if (LUS_LUSI)
127
      add_custom_command(
128
         OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}i
129
         COMMAND ${LUSTRE_COMPILER} ${LUSTRE_LUSI_OPT} ${LFILE}
130
         DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}
131
         WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
132
         COMMENT "Compile Lustre source(s): ${LFILE} with option -lusi."
133
         )
134
      message(STATUS "lustrec will produce lusi file: ${LFILE}i")
135
    endif()
136
    add_custom_command(
137
      OUTPUT ${LUSTRE_GENERATED_FILES}
138
      COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}
139
      DEPENDS ${LFILE}
140
      WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
141
      COMMENT "Compile Lustre source(s): ${LFILE} (generates: ${LUSTRE_GENERATED_FILES})."
142
      )
143
    set_source_files_properties(${LUSTRE_GENERATED_FILES} PROPERTIES GENERATED TRUE)
144
  endforeach()
145

  
146
  include_directories(${LUSTRE_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${LUSTRE_OUTPUT_DIR})
147
  if(LUS_NODE)
148
  add_executable(${LUS_LIBNAME}
149
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${GLOBAL_LUSTRE_DEP_FILES} ${LUS_USER_C_FILES}
150
              )
151
  else()
152
  add_library(${LUS_LIBNAME} SHARED
153
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${GLOBAL_LUSTRE_DEP_FILES} ${LUS_USER_C_FILES}
154
              )
155
  endif()
156
  set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99")
157
  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE)
158
  message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}")
159
endfunction(Lustre_Compile)
160

  
161
# handle the QUIETLY and REQUIRED arguments and set LUSTRE_FOUND to TRUE if
162
# all listed variables are TRUE
163
include(FindPackageHandleStandardArgs)
164
FIND_PACKAGE_HANDLE_STANDARD_ARGS(LUSTRE
165
                                  REQUIRED_VARS LUSTRE_COMPILER LUSTRE_INCLUDE_DIR)
166
# VERSION FPHSA options not handled by CMake version < 2.8.2)
167
#                                  VERSION_VAR LUSTRE_COMPILER_VERSION)
168
mark_as_advanced(LUSTRE_INCLUDE_DIR)
share/FindLustre.cmake.in
1
# - Find Lustre compiler
2
# Find the Lustre synchronous language compiler with associated includes path.
3
# See https://cavale.enseeiht.fr/redmine/projects/lustrec
4
# This module defines
5
#  LUSTRE_COMPILER, the lustre compiler
6
#  LUSTRE_COMPILER_VERSION, the version of the lustre compiler
7
#  LUSTRE_INCLUDE_DIR, where to find dword.h, etc.
8
#  LUSTRE_FOUND, If false, Lustre was not found.
9
# On can set LUSTRE_PATH_HINT before using find_package(Lustre) and the
10
# module with use the PATH as a hint to find lustrec.
11
#
12
# The hint can be given on the command line too:
13
#   cmake -DLUSTRE_PATH_HINT=/DATA/ERIC/Lustre/lustre-x.y /path/to/source
14
#
15
# The module defines some functions:
16
#   Lustre_Compile([NODE <Lustre Main Node>]
17
#                  LUS_FILES <Lustre files>
18
#                  [USER_C_FILES <C files>]
19
#                  [VERBOSE <level>]
20
#                  [LUSI]
21
#                  LIBNAME <libraryName>)
22
#
23
# When used the Lustre_Compile macro define the variable
24
# LUSTRE_GENERATED_C_FILES_<libraryName> in the parent scope
25
# so that the caller can get (if needed) the list of Lustre generated files.
26
# The VERBOSE level is a numeric value passed directly to the -verbose
27
# command line option of the lustre compiler
28
#
29
include("@prefix@/share/helpful_functions.cmake")
30

  
31
if(LUSTRE_PATH_HINT)
32
  message(STATUS "FindLustre: using PATH HINT: ${LUSTRE_PATH_HINT}")
33
else()
34
  set(LUSTRE_PATH_HINT)
35
endif()
36

  
37
#One can add his/her own builtin PATH.
38
#FILE(TO_CMAKE_PATH "/DATA/ERIC/Lustre/lustre-x.y" MYPATH)
39
#list(APPEND LUSTRE_PATH_HINT ${MYPATH})
40

  
41
# FIND_PROGRAM twice using NO_DEFAULT_PATH on first shot
42
find_program(LUSTRE_COMPILER
43
  NAMES lustrec
44
  PATHS ${LUSTRE_PATH_HINT}
45
  PATH_SUFFIXES bin
46
  NO_DEFAULT_PATH
47
  DOC "Path to the Lustre compiler command 'lustrec'")
48

  
49
find_program(LUSTRE_COMPILER
50
  NAMES lustrec
51
  PATHS ${LUSTRE_PATH_HINT}
52
  PATH_SUFFIXES bin
53
  DOC "Path to the Lustre compiler command 'lustrec'")
54

  
55
if(LUSTRE_COMPILER)
56
    # get the path where the lustre compiler was found
57
    get_filename_component(LUSTRE_PATH ${LUSTRE_COMPILER} PATH)
58
    # remove bin
59
    get_filename_component(LUSTRE_PATH ${LUSTRE_PATH} PATH)
60
    # add path to LUSTRE_PATH_HINT
61
    list(APPEND LUSTRE_PATH_HINT ${LUSTRE_PATH})
62
    execute_process(COMMAND ${LUSTRE_COMPILER} -version
63
        OUTPUT_VARIABLE LUSTRE_COMPILER_VERSION
64
        OUTPUT_STRIP_TRAILING_WHITESPACE)
65
    message(STATUS "Lustre compiler version is : ${LUSTRE_COMPILER_VERSION}")
66
endif(LUSTRE_COMPILER)
67

  
68
find_path(LUSTRE_INCLUDE_DIR
69
          NAMES arrow.h
70
          PATHS ${LUSTRE_PATH_HINT}
71
          PATH_SUFFIXES include/lustrec
72
          DOC "The Lustre include headers")
73

  
74
# Macros used to compile a lustre library
75
include(CMakeParseArguments)
76
function(Lustre_Compile)
77
  set(options LUSI)
78
  set(oneValueArgs NODE LIBNAME VERBOSE)
79
  set(multiValueArgs LUS_FILES USER_C_FILES)
80
  cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
81

  
82
  if(LUS_LUSI)
83
    set(LUSTRE_LUSI_OPT "-lusi")
84
  endif()
85

  
86
  if (NOT LUS_LIBNAME)
87
    message(FATAL_ERROR "You should specify LIBNAME for each Lustre_Compile call.")
88
  endif()
89

  
90
  if(LUS_NODE)
91
    set(LUSTRE_NODE_OPT "-node;${LUS_NODE}")
92
    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}/${LUS_NODE}")
93
  else()
94
    set(LUSTRE_NODE_OPT "")
95
    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}")
96
  endif()
97

  
98
  if (LUS_VERBOSE)
99
    set(LUSTRE_VERBOSE_OPT "-verbose;${LUS_VERBOSE}")
100
  else()
101
    # the default is to be quiet.
102
    set(LUSTRE_VERBOSE_OPT "-verbose;0")
103
  endif()
104

  
105
  file(MAKE_DIRECTORY ${LUSTRE_OUTPUT_DIR})
106
  set(GLOBAL_LUSTRE_GENERATED_C_FILES "")
107
  set(GLOBAL_LUSTRE_DEP_C_FILES "")
108
  # create list of generated C files in parent scope
109
  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "" PARENT_SCOPE)
110
  foreach(LFILE IN LISTS LUS_LUS_FILES)
111
    get_lustre_name_ext(${LFILE} L E)
112
    
113
    if ("${E}" STREQUAL "lus")
114
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h ${LUSTRE_OUTPUT_DIR}/${L}.c ${LUSTRE_OUTPUT_DIR}/${L}_alloc.h)
115
      set(LUSTRE_DEP_FILES "")
116
      if(LUS_NODE)
117
         list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}_main.c)
118
         list(APPEND LUSTRE_DEP_FILES ${LUSTRE_INCLUDE_DIR}/io_frontend.c)
119
      endif()
120
    elseif("${E}" STREQUAL "lusi")
121
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h)
122
    endif()
123
    list(APPEND GLOBAL_LUSTRE_GENERATED_C_FILES ${LUSTRE_GENERATED_FILES})
124
    list(APPEND GLOBAL_LUSTRE_DEP_FILES ${LUSTRE_DEP_FILES}) # todo: add if not already in the list
125
    set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic)
126
    if (LUS_LUSI)
127
      add_custom_command(
128
         OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}i
129
         COMMAND ${LUSTRE_COMPILER} ${LUSTRE_LUSI_OPT} ${LFILE}
130
         DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}
131
         WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
132
         COMMENT "Compile Lustre source(s): ${LFILE} with option -lusi."
133
         )
134
      message(STATUS "lustrec will produce lusi file: ${LFILE}i")
135
    endif()
136
    add_custom_command(
137
      OUTPUT ${LUSTRE_GENERATED_FILES}
138
      COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}
139
      DEPENDS ${LFILE}
140
      WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
141
      COMMENT "Compile Lustre source(s): ${LFILE} (generates: ${LUSTRE_GENERATED_FILES})."
142
      )
143
    set_source_files_properties(${LUSTRE_GENERATED_FILES} PROPERTIES GENERATED TRUE)
144
  endforeach()
145

  
146
  include_directories(${LUSTRE_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${LUSTRE_OUTPUT_DIR})
147
  if(LUS_NODE)
148
  add_executable(${LUS_LIBNAME}
149
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${GLOBAL_LUSTRE_DEP_FILES} ${LUS_USER_C_FILES}
150
              )
151
  else()
152
  add_library(${LUS_LIBNAME} SHARED
153
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${GLOBAL_LUSTRE_DEP_FILES} ${LUS_USER_C_FILES}
154
              )
155
  endif()
156
  set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99")
157
  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE)
158
  message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}")
159
endfunction(Lustre_Compile)
160

  
161
# handle the QUIETLY and REQUIRED arguments and set LUSTRE_FOUND to TRUE if
162
# all listed variables are TRUE
163
include(FindPackageHandleStandardArgs)
164
FIND_PACKAGE_HANDLE_STANDARD_ARGS(LUSTRE
165
                                  REQUIRED_VARS LUSTRE_COMPILER LUSTRE_INCLUDE_DIR)
166
# VERSION FPHSA options not handled by CMake version < 2.8.2)
167
#                                  VERSION_VAR LUSTRE_COMPILER_VERSION)
168
mark_as_advanced(LUSTRE_INCLUDE_DIR)
src/automata.ml
263 263
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
264 264

  
265 265
let expand_node_stmts nused used loc owner node =
266
  let (top_types', top_nodes', locals', eqs') =
266
  let top_types', top_nodes', locals', eqs' =
267 267
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
268 268
  let node' = 
269 269
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
......
277 277
    match top_decl.top_decl_desc with
278 278
    | Node nd ->
279 279
      let used name =
280
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
281
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
282
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
283
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
280
        List.exists (fun v -> v.var_id = name) nd.node_inputs
281
        || List.exists (fun v -> v.var_id = name) nd.node_outputs
282
        || List.exists (fun v -> v.var_id = name) nd.node_locals in
283
      let top_types', top_decl', top_nodes' = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
284 284
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
285 285
    | _       -> top_decl :: expand_decls_rec nused q
286 286

  
287 287
let expand_decls top_decls =
288 288
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
289
    | Node nd         -> ISet.add nd.node_id names
290
    | ImportedNode nd -> ISet.add nd.nodei_id names
291
    | _               -> names) ISet.empty top_decls in
289
      | Node nd         -> ISet.add nd.node_id names
290
      | ImportedNode nd -> ISet.add nd.nodei_id names
291
      | _               -> names) ISet.empty top_decls in
292 292
  let nused name = ISet.mem name top_names in
293 293
  expand_decls_rec nused top_decls
294 294

  
src/backends/C/c_backend_header.ml
280 280
		| _        -> ()) type_table
281 281

  
282 282
let reset_type_definitions, print_type_definition_from_header =
283
  let cpt_type =ref 0 in
284
  ((fun () -> cpt_type := 0),
285
   (fun fmt typ filename ->
286
    fprintf fmt "typedef %a;@.@."
287
	(pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc))
283
  let cpt_type = ref 0 in
284
  (fun () -> cpt_type := 0),
285
  (fun fmt typ filename ->
286
     fprintf fmt "typedef %a;@.@."
287
	     (pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc)
288 288

  
289 289
(********************************************************************************************)
290 290
(*                         MAIN Header Printing functions                                   *)
src/backends/C/c_backend_makefile.ml
98 98
    fprintf fmt "GCC=gcc -O0@.";
99 99
    fprintf fmt "LUSTREC=%s@." Sys.executable_name;
100 100
    fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
101
    fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
101
    fprintf fmt "INC=%s@." Version.include_path (*"${LUSTREC_BASE}/include/lustrec"*);
102 102
    fprintf fmt "@.";
103 103

  
104 104
    (* Main binary *)
src/compiler_stages.ml
17 17
  let destname = !Options.dest_dir ^ "/" ^ basename in
18 18
  let lusic_ext = ".lusic" in
19 19
  let header_name = destname ^ lusic_ext in
20
  let from_lusi = extension = ".lusi" in
20 21
  begin
21 22
    if (* Generating the lusic file *)
22
      extension = ".lusi" (* because input is a lusi *)
23
      || (extension = ".lus" &&
24
            not (Sys.file_exists header_name))
25
           (* or because it is a lus but not lusic exists *)
23
      (* because input is a lusi *)
24
      from_lusi
25
      (* or because it is a lus but no lusic exists *)
26
      || (extension = ".lus" && not (Sys.file_exists header_name))
27
      (* or the lusic exists but is not generated from a lusi, hence it
28
         has te be regenerated *)
26 29
      || (let lusic = Lusic.read_lusic destname lusic_ext in
27 30
          not lusic.Lusic.from_lusi)
28
         (* or the lusic exists but is not generated from a lusi, hence it
29
            has te be regenerated *)
30 31
    then
31 32
      begin
32
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
33
	Lusic.write_lusic
34
          (extension = ".lusi") (* is it a lusi file ? *)
35
          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)
33
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
34
        Lusic.write_lusic
35
          from_lusi (* is it a lusi file ? *)
36
          (if from_lusi then prog else Lusic.extract_header dirname basename prog)
36 37
          destname
37 38
          lusic_ext;
38
        let _ =
39
          match !Options.output with
40
          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
41
          | _ -> ()
42
        in
43
        ()
39
        match !Options.output with
40
        | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
41
        | _ -> ()
44 42
      end
45 43
    else (* Lusic exists and is usable. Checking compatibility *)
46 44
      begin
47
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
45
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
48 46
        let lusic = Lusic.read_lusic destname lusic_ext in
49 47
        Lusic.check_obsolete lusic destname;
50
	let header = lusic.Lusic.contents in
51
	let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
52
	check_compatibility
53
	  (prog, computed_types_env, computed_clocks_env)
54
	  (header, declared_types_env, declared_clocks_env)
48
        let header = lusic.Lusic.contents in
49
        let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
50
        check_compatibility
51
          (prog, computed_types_env, computed_clocks_env)
52
          (header, declared_types_env, declared_clocks_env)
55 53
      end
56 54
  end
57 55

  
src/dune
50 50
   clock_calculus
51 51
 )
52 52
 (wrapped false)
53
 (libraries ocamlgraph zarith unix str))
53
 (libraries sites ocamlgraph zarith unix str))
54 54

  
55 55
(library
56 56
 (name plugin_register)
......
61 61

  
62 62
(generate_sites_module
63 63
 (module sites)
64
 (plugins (lustrec plugins) (lustrec verifiers)))
64
 ; (sites lustrec)
65
 (plugins
66
  (lustrec plugins)
67
  (lustrec verifiers)))
65 68

  
66 69
(library
67 70
 (name sites)
......
157 160
   memo)
158 161
 (libraries tools_lib))
159 162

  
163

  
164

  
160 165
; (executable
161 166
;  (name main_parse_json_file)
162 167
;  (public_name json-parser)
src/lusic.ml
32 32
  let owner = dirname ^ "/" ^ basename in
33 33
  List.fold_right
34 34
    (fun decl header ->
35
      (*Format.eprintf "Lusic.extract_header: header = %B, owner = %s, decl_owner = %s@." decl.top_decl_itf owner decl.top_decl_owner;*)
36
      if decl.top_decl_itf || decl.top_decl_owner <> owner then header else
37
	match decl.top_decl_desc with
38
	| Node nd        -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header 
39
	| ImportedNode _ -> header
40
	| Const _
41
	| TypeDef _
42
	| Include _ | Open _         -> decl :: header)
35
       (* Format.eprintf "Lusic.extract_header: header = %B, owner = %s, decl_owner = %s@."
36
        *   decl.top_decl_itf owner decl.top_decl_owner; *)
37
       if decl.top_decl_itf || decl.top_decl_owner <> owner then header
38
       else match decl.top_decl_desc with
39
         | Node nd ->
40
           { decl with top_decl_desc =
41
                         ImportedNode (Corelang.get_node_interface nd) }
42
           :: header
43
         | ImportedNode _ -> header
44
         | Const _ | TypeDef _ | Include _ | Open _  -> decl :: header)
43 45
    prog []
44 46

  
45 47
let check_obsolete lusic basename =
src/main_lustre_testgen.ml
152 152
  let cmake_file = open_out cmakelists in
153 153
  let cmake_fmt = formatter_of_out_channel cmake_file in
154 154
  Format.fprintf cmake_fmt "cmake_minimum_required(VERSION 3.5)@.";
155
  Format.fprintf cmake_fmt "include(\"%s/share/helpful_functions.cmake\")@." Version.prefix;
156
  Format.fprintf cmake_fmt "include(\"%s/share/FindLustre.cmake\")@." Version.prefix;
155
  Format.fprintf cmake_fmt "include(\"%s/helpful_functions.cmake\")@." Version.testgen_path;
156
  Format.fprintf cmake_fmt "include(\"%s/FindLustre.cmake\")@." Version.testgen_path;
157 157
  Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@.";
158 158
  Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ ";
159 159
  Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ ";
src/options_management.ml
11 11
open Options
12 12

  
13 13
let print_version () =
14
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
14
  Format.printf "Lustrec compiler, version %s (%s)@." version (codename ());
15 15
  Format.printf "Standard lib: %s@." Version.include_path;
16 16
  Format.printf "User provided include directory: @[<h>%a@]@."
17 17
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) !include_dirs
src/parsers/parse.ml
24 24

  
25 25
exception Error of (Location.t * error)
26 26

  
27

  
28 27
let pp_error fmt err =
29 28
  match err with
30
  | Unexpected_eof          -> fprintf fmt "unexpected end of file"
31
  | Undefined_token tok   -> fprintf fmt "undefined token '%s'" tok
32
  | Unfinished_string        -> fprintf fmt "unfinished string"
33
  | Unfinished_comment  -> fprintf fmt "unfinished comment"
34
  | Syntax_error               -> fprintf fmt "syntax error"
35
  | String_Syntax_error s              -> fprintf fmt "syntax error in %s" s
36
  | Unfinished_annot        -> fprintf fmt "unfinished annotation"
37
  | Unfinished_node_spec -> fprintf fmt "unfinished node specification"
38
  | Annot_error s              -> fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s
39
  | Node_spec_error s       -> fprintf fmt "Impossible to parse the following node specification:@.%s@.@?" s
29
  | Unexpected_eof ->
30
    fprintf fmt "unexpected end of file"
31
  | Undefined_token tok ->
32
    fprintf fmt "undefined token '%s'" tok
33
  | Unfinished_string ->
34
    fprintf fmt "unfinished string"
35
  | Unfinished_comment ->
36
    fprintf fmt "unfinished comment"
37
  | Syntax_error ->
38
    fprintf fmt "syntax error"
39
  | String_Syntax_error s ->
40
    fprintf fmt "syntax error in %s" s
41
  | Unfinished_annot ->
42
    fprintf fmt "unfinished annotation"
43
  | Unfinished_node_spec ->
44
    fprintf fmt "unfinished node specification"
45
  | Annot_error s ->
46
    fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s
47
  | Node_spec_error s ->
48
    fprintf fmt "Impossible to parse the following node specification:@.%s@.@?" s
40 49

  
41 50
let report_error (loc, err) =
42
  eprintf "Syntax error: %a@.%a@."
43
    pp_error err
51
  eprintf "Syntax error: %a@."
52
    (* pp_error err *)
44 53
    Location.pp_loc loc
45 54

  
46 55
let header parsing_fun token_fun lexbuf =
47
  try
48
    let ast = parsing_fun token_fun lexbuf in
49
    Parsing.clear_parser ();
50
    ast
51
  with
52
  | Parsing.Parse_error ->
56
  try parsing_fun token_fun lexbuf with _ ->
53 57
    let loc = Location.curr lexbuf in
54
    raise (Error (loc, Syntax_error))
58
    let e = loc, Syntax_error in
59
    report_error e;
60
    raise (Error e)
55 61

  
56 62
let prog parsing_fun token_fun lexbuf =
57
  try
58
    let ast = parsing_fun token_fun lexbuf in
59
    Parsing.clear_parser ();
60
    ast
61
  with
62
  | Parsing.Parse_error ->
63
  try parsing_fun token_fun lexbuf with err ->
63 64
    let loc = Location.curr lexbuf in
64
    raise (Error (loc, Syntax_error))
65
    let e = loc, Syntax_error in
66
    report_error e;
67
    raise (Error e)
65 68

  
66 69
(* Local Variables: *)
67 70
(* compile-command:"make -C .." *)
src/parsers/parser_lustre.mly
19 19
let get_loc () = Location.symbol_rloc ()
20 20

  
21 21
let mkident x = x, get_loc ()
22
let mktyp = mktyp (get_loc ())
22
let mktyp x = mktyp (get_loc ()) x
23 23
let mkotyp x = match x with Some t -> Some (mktyp t) | None -> None
24
let mkclock = mkclock (get_loc ())
24
let mkclock x = mkclock (get_loc ()) x
25 25
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
26
let mkexpr = mkexpr (get_loc ())
27
let mkeexpr = mkeexpr (get_loc ())
28
let mkeq = mkeq (get_loc ())
29
let mkassert = mkassert (get_loc ())
30
let mktop_decl = mktop_decl (get_loc ()) (Location.get_module ())
31
let mkpredef_call = mkpredef_call (get_loc ())
26
let mkexpr x = mkexpr (get_loc ()) x
27
let mkeexpr x = mkeexpr (get_loc ()) x
28
let mkeq x = mkeq (get_loc ()) x
29
let mkassert x = mkassert (get_loc ()) x
30
let mktop_decl x = mktop_decl (get_loc ()) (Location.get_module ()) x
31
let mkpredef_call x = mkpredef_call (get_loc ()) x
32 32
let mkpredef_call_b f x1 x2 = mkpredef_call f [x1; x2]
33 33
let mkpredef_call_u f x = mkpredef_call f [x]
34 34

  
35
let mkdim_int = mkdim_int (get_loc ())
35
let mkdim_int x = mkdim_int (get_loc ()) x
36 36
(* let mkdim_bool b = mkdim_bool (get_loc ()) b *)
37
let mkdim_ident = mkdim_ident (get_loc ())
38
let mkdim_appl = mkdim_appl (get_loc ())
37
let mkdim_ident x = mkdim_ident (get_loc ()) x
38
let mkdim_appl x = mkdim_appl (get_loc ()) x
39 39
let mkdim_appl_b f x1 x2 = mkdim_appl f [x1; x2]
40 40
let mkdim_appl_u f x = mkdim_appl f [x]
41
let mkdim_ite = mkdim_ite (get_loc ())
41
let mkdim_ite x = mkdim_ite (get_loc ()) x
42 42

  
43 43
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))
44 44

  
......
96 96
%token EOF
97 97

  
98 98
%nonassoc p_string
99
%nonassoc p_vdecl
100
%left SCOL
99
(* %nonassoc p_vdecl *)
100
(* %left SCOL *)
101 101
%nonassoc EVERY
102 102
%nonassoc ELSE
103 103
%right ARROW FBY
......
189 189
| CONST ds=cdecl+ SCOL
190 190
  { List.map ((|>) true) ds }
191 191
| nodei_spec=nodespecs nodei_stateless=state_annot nodei_id=node_ident_decl
192
  LPAR nodei_inputs=vdecl_list SCOL? RPAR
193
  RETURNS LPAR nodei_outputs=vdecl_list SCOL? RPAR
192
  LPAR nodei_inputs=var_decl_list(vdecl) RPAR
193
  RETURNS LPAR nodei_outputs=var_decl_list(vdecl) RPAR
194 194
  nodei_prototype=preceded(PROTOTYPE, node_ident)?
195 195
  nodei_in_lib=preceded(LIB, module_ident)* SCOL
196 196
  { let nd = mktop_decl true (ImportedNode {
......
215 215
| CONST ds=cdecl+ SCOL
216 216
  { List.map ((|>) false) ds }
217 217
| node_dec_stateless=state_annot node_id=node_ident_decl
218
  LPAR node_inputs=vdecl_list SCOL? RPAR
219
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
218
  LPAR node_inputs=var_decl_list(vdecl) RPAR
219
  RETURNS LPAR node_outputs=var_decl_list(vdecl) RPAR SCOL?
220 220
  node_spec=nodespecs
221 221
  node_locals=locals LET content=stmt_list TEL
222 222
  { let node_stmts, node_asserts, node_annot = content in
......
351 351

  
352 352
top_contract:
353 353
| CONTRACT node_id=node_ident_decl
354
  LPAR node_inputs=vdecl_list SCOL? RPAR
355
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
354
  LPAR node_inputs=var_decl_list(vdecl) RPAR
355
  RETURNS LPAR node_outputs=var_decl_list(vdecl) RPAR SCOL?
356 356
  LET cc=contract_content TEL
357 357
  { let nd = mktop_decl true (Node {
358 358
                                  node_id;
......
566 566
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite d t f }
567 567

  
568 568
%inline locals:
569
| xs=loption(preceded(VAR, flatten(separated_nonempty_list(SCOL, local_vdecl))))
570
  { xs }
569
| xs=loption(preceded(VAR, var_decl_list(local_vdecl))) { xs }
571 570

  
572
vdecl_list:
573
| d=vdecl %prec p_vdecl { d }
574
| d=vdecl SCOL ds=vdecl_list { d @ ds }
571
var_decl_list(X):
572
| d=X ioption(SCOL)            { d }
573
| d=X SCOL ds=var_decl_list(X) { d @ ds }
575 574

  
576 575
vdecl:
577 576
| xs=ident_list COL t=typeconst c=clock?
src/utils/location.ml
90 90
  let (start_char, end_char) =
91 91
    if start_char < 0 then (0,1) else (start_char, end_char)
92 92
  in
93
  Format.fprintf fmt "File \"%s\", line %i, characters %i-%i:" filename line start_char end_char;
93
  Format.fprintf fmt "File \"%s\", line %i, characters %i-%i"
94
    filename line start_char end_char;
94 95
  (* Format.fprintf fmt "@.loc1=(%i,%i,%i) loc2=(%i,%i,%i)@."
95 96
   *   loc.loc_start.Lexing.pos_lnum
96 97
   *   loc.loc_start.Lexing.pos_bol
src/version.ml
1
let number = "@PACKAGE_VERSION@-@GITBRANCH@"
1
let number = "%%VERSION%%"
2 2

  
3
let codename ="@VERSION_CODENAME@"
3
let codename () =
4
  match "%%VERSION_NUM%%" with
5
  | "1.7" -> "Xia/Huai-dev"
6
  | _ -> "dev"
4 7

  
5
let prefix = "@prefix@"
6

  
7
let include_path = prefix ^ "/include/lustrec"
8
let include_path = Sites.Sites.include_ |> List.hd
9
let testgen_path = Sites.Sites.testgen |> List.hd
tests
1
Subproject commit 0ac53ee0fbfc6ba8261ad8ab15173bd58c4d043c

Also available in: Unified diff