|
1
|
cmake_minimum_required(VERSION 2.8.4)
|
|
2
|
include(FindUnixCommands)
|
|
3
|
|
|
4
|
|
|
5
|
if(ZUSTRE_COMPILER)
|
|
6
|
message(STATUS "Found zustre: ${ZUSTRE_COMPILER} ")
|
|
7
|
else(ZUSTRE_COMPILER)
|
|
8
|
message(FATAL_ERROR "zustre not found")
|
|
9
|
endif(ZUSTRE_COMPILER)
|
|
10
|
|
|
11
|
|
|
12
|
|
|
13
|
|
|
14
|
#first combination :no option
|
|
15
|
set(ZUSTRE_OPTIONS_OPT "--timeout" "60" "--xml" )
|
|
16
|
#take all lustre files
|
|
17
|
set(GLOBAL_LUSTRE_FILES "")
|
|
18
|
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
|
|
19
|
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
|
|
20
|
FOREACH(lfile ${LFILES})
|
|
21
|
get_filename_component(L ${lfile} NAME_WE)
|
|
22
|
set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
|
|
23
|
file(COPY ${lfile} DESTINATION ${LUSTRE_OUTPUT_DIR})
|
|
24
|
if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
|
|
25
|
file(COPY ${L}.lusi DESTINATION ${LUSTRE_OUTPUT_DIR})
|
|
26
|
else()
|
|
27
|
message("generate ${L}.lusi \n")
|
|
28
|
Lustre_Compile(LUS_FILE ${lfile}
|
|
29
|
NODE ""
|
|
30
|
OPTS "-lusi")
|
|
31
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
|
32
|
execute_process(RESULT_VARIABLE res
|
|
33
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}}
|
|
34
|
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
|
|
35
|
if(${res} STREQUAL "0")
|
|
36
|
file(COPY ${L}.lusi DESTINATION ${LUSTRE_OUTPUT_DIR})
|
|
37
|
else()
|
|
38
|
message("${L}.lusi Error")
|
|
39
|
endif()
|
|
40
|
endif()
|
|
41
|
|
|
42
|
if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml)
|
|
43
|
file(COPY ${L}.xml DESTINATION ${LUSTRE_OUTPUT_DIR})
|
|
44
|
file(READ ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${L}_zustre_output)
|
|
45
|
else()
|
|
46
|
message("generate ${L}.xml for reference\n")
|
|
47
|
Zustre_Compile(LUS_FILE ${lfile}
|
|
48
|
NODE "top"
|
|
49
|
OPTS ${ZUSTRE_OPTIONS_OPT})
|
|
50
|
set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
|
|
51
|
execute_process(RESULT_VARIABLE res
|
|
52
|
OUTPUT_VARIABLE ${L}_zustre_output
|
|
53
|
COMMAND ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_top_${ZUS_OPTS_CUT}}
|
|
54
|
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
|
|
55
|
|
|
56
|
file(WRITE ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${${L}_zustre_output})
|
|
57
|
file(COPY ${L}.xml DESTINATION ${LUSTRE_OUTPUT_DIR})
|
|
58
|
message("${${L}_zustre_output}")
|
|
59
|
endif()
|
|
60
|
if( ${${L}_zustre_output} MATCHES "<Answer>CEX</Answer>")
|
|
61
|
#message("${L}.xml is CEX")
|
|
62
|
set(ZUSTRE_ANSWER_${L} "CEX")
|
|
63
|
elseif( ${${L}_zustre_output} MATCHES "<Answer>SAFE</Answer>")
|
|
64
|
#message("${L}.xml is SAFE")
|
|
65
|
set(ZUSTRE_ANSWER_${L} "SAFE")
|
|
66
|
elseif( ${${L}_zustre_output} MATCHES "<Answer>TIMEOUT</Answer>")
|
|
67
|
#message("${L}.xml is TIMEOUT")
|
|
68
|
set(ZUSTRE_ANSWER_${L} "TIMEOUT")
|
|
69
|
else()
|
|
70
|
#message("${L}.xml is Error")
|
|
71
|
set(ZUSTRE_ANSWER_${L} "ERROR")
|
|
72
|
endif()
|
|
73
|
ENDFOREACH()
|
|
74
|
|
|
75
|
|
|
76
|
|
|
77
|
|
|
78
|
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
|
|
79
|
get_filename_component(L ${lus_file} NAME_WE)
|
|
80
|
set(ZUSTRE_NODE_OPT "top")
|
|
81
|
|
|
82
|
Lustre_Compile(LUS_FILE ${lus_file}
|
|
83
|
NODE ""
|
|
84
|
OPTS "-horn")
|
|
85
|
|
|
86
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
|
87
|
add_test(NAME Kind_fmcad08_misc_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
|
|
88
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}}
|
|
89
|
)
|
|
90
|
|
|
91
|
Zustre_Compile(LUS_FILE ${lus_file}
|
|
92
|
NODE ${ZUSTRE_NODE_OPT}
|
|
93
|
OPTS ${ZUSTRE_OPTIONS_OPT})
|
|
94
|
set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
|
|
95
|
set(ZUSTRE_OUTPUT_DIR ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}})
|
|
96
|
|
|
97
|
set(ZUSTRE_ARGS_TEMP "${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}" "> ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml")
|
|
98
|
JOIN("${ZUSTRE_ARGS_TEMP}" " " ZUSTRE_ARGS)
|
|
99
|
|
|
100
|
add_test(NAME Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
101
|
COMMAND bash -c "${ZUSTRE_COMPILER} ${ZUSTRE_ARGS}"
|
|
102
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
103
|
)
|
|
104
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
105
|
PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
|
|
106
|
DEPENDS Kind_fmcad08_misc_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
|
|
107
|
|
|
108
|
|
|
109
|
add_test(NAME Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
110
|
COMMAND bash -c "tail -n +8 ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml > ${L}_tailed1.xml"
|
|
111
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
112
|
#DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
113
|
)
|
|
114
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
115
|
PROPERTIES REQUIRED_FILES ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
|
116
|
DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
|
117
|
|
|
118
|
add_test(NAME Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
119
|
COMMAND bash -c "tail -n +8 ${L}.xml > ${L}_tailed2.xml"
|
|
120
|
WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${L}/
|
|
121
|
)
|
|
122
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
123
|
PROPERTIES REQUIRED_FILES ${L}.xml
|
|
124
|
DEPENDS Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
|
125
|
|
|
126
|
|
|
127
|
add_test(NAME Kind_fmcad08_misc_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
128
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_tailed1.xml ../${L}_tailed2.xml
|
|
129
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
130
|
)
|
|
131
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
132
|
PROPERTIES REQUIRED_FILES ${L}_tailed1.xml
|
|
133
|
DEPENDS Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
|
134
|
|
|
135
|
|
|
136
|
if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class AND ${ZUSTRE_ANSWER_${L}} STREQUAL "CEX" AND EXISTS ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi)
|
|
137
|
#message("add tests for comaring Zustre and lustrec in memory")
|
|
138
|
add_test(NAME Kind_fmcad08_misc_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
139
|
COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ XPathParser_lusi ${ZUSTRE_NODE_OPT} ../${L}.lusi ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
|
140
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
141
|
)
|
|
142
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
|
143
|
PROPERTIES REQUIRED_FILES ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi
|
|
144
|
DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT} )
|
|
145
|
|
|
146
|
set(LUSTRE_NODE_OPT "top")
|
|
147
|
# First command generate C files from Lustre file
|
|
148
|
Lustre_Compile(LUS_FILE ${lus_file}
|
|
149
|
NODE ${LUSTRE_NODE_OPT}
|
|
150
|
OPTS ""
|
|
151
|
DIR ${ZUSTRE_OUTPUT_DIR})
|
|
152
|
|
|
153
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
|
154
|
add_test(NAME Kind_fmcad08_misc_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
155
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
|
|
156
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
157
|
)
|
|
158
|
|
|
159
|
#********************* make -f ${L}.makefile ***************************
|
|
160
|
add_test(NAME Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
161
|
COMMAND make -f ${L}.makefile
|
|
162
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
163
|
)
|
|
164
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
165
|
PROPERTIES DEPENDS Kind_fmcad08_misc_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
166
|
REQUIRED_FILES ${L}.makefile
|
|
167
|
)
|
|
168
|
|
|
169
|
#************** execute C binary **********************************
|
|
170
|
|
|
171
|
if (BASH)
|
|
172
|
add_test(
|
|
173
|
NAME Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
174
|
COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
|
|
175
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
176
|
)
|
|
177
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
178
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
|
|
179
|
DEPENDS Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
|
|
180
|
else()
|
|
181
|
message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
|
|
182
|
endif()
|
|
183
|
|
|
184
|
#************** execute C binary **********************************
|
|
185
|
add_test(NAME Kind_fmcad08_misc_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
186
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ZUSTRE_output_values
|
|
187
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
|
188
|
)
|
|
189
|
SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
|
190
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
|
|
191
|
DEPENDS Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
|
|
192
|
|
|
193
|
|
|
194
|
|
|
195
|
endif()
|
|
196
|
|
|
197
|
ENDFOREACH()
|
|
198
|
add_custom_target(Kind_fmcad08_misc COMMAND ${CMAKE_CTEST_COMMAND} -R Kind_fmcad08_misc)
|