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
|
if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml)
|
42
|
file(COPY ${L}.xml DESTINATION ${LUSTRE_OUTPUT_DIR})
|
43
|
else()
|
44
|
message("generate ${L}.xml for reference\n")
|
45
|
Zustre_Compile(LUS_FILE ${lfile}
|
46
|
NODE "top"
|
47
|
OPTS ${ZUSTRE_OPTIONS_OPT})
|
48
|
set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
|
49
|
execute_process(RESULT_VARIABLE res
|
50
|
OUTPUT_VARIABLE ${L}_output
|
51
|
COMMAND ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_top_${ZUS_OPTS_CUT}}
|
52
|
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
|
53
|
if(${res} STREQUAL "0")
|
54
|
if( ${${L}_output} MATCHES "<Answer>CEX</Answer>")
|
55
|
message("${L} CEX")
|
56
|
file(WRITE ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${${L}_output})
|
57
|
file(COPY ${L}.xml DESTINATION ${LUSTRE_OUTPUT_DIR})
|
58
|
else()
|
59
|
message("${L} is not CEX\n ${${L}_output}")
|
60
|
endif()
|
61
|
else()
|
62
|
message("${L}.xml Error")
|
63
|
endif()
|
64
|
endif()
|
65
|
|
66
|
ENDFOREACH()
|
67
|
|
68
|
|
69
|
|
70
|
|
71
|
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
|
72
|
get_filename_component(L ${lus_file} NAME_WE)
|
73
|
set(ZUSTRE_NODE_OPT "top")
|
74
|
|
75
|
Lustre_Compile(LUS_FILE ${lus_file}
|
76
|
NODE ""
|
77
|
OPTS "-horn")
|
78
|
|
79
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
80
|
add_test(NAME kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
|
81
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}}
|
82
|
)
|
83
|
|
84
|
Zustre_Compile(LUS_FILE ${lus_file}
|
85
|
NODE ${ZUSTRE_NODE_OPT}
|
86
|
OPTS ${ZUSTRE_OPTIONS_OPT})
|
87
|
set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
|
88
|
set(ZUSTRE_OUTPUT_DIR ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}})
|
89
|
|
90
|
set(ZUSTRE_ARGS_TEMP "${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}" "> ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml")
|
91
|
JOIN("${ZUSTRE_ARGS_TEMP}" " " ZUSTRE_ARGS)
|
92
|
|
93
|
add_test(NAME kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
94
|
COMMAND bash -c "${ZUSTRE_COMPILER} ${ZUSTRE_ARGS}"
|
95
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
96
|
)
|
97
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
98
|
PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
|
99
|
DEPENDS kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
|
100
|
|
101
|
|
102
|
add_test(NAME kind_fmcad08_large_CEX_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
103
|
COMMAND bash -c "tail -n +8 ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml > ${L}_tailed1.xml"
|
104
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
105
|
#DEPENDS kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
106
|
)
|
107
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
108
|
PROPERTIES REQUIRED_FILES ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
109
|
DEPENDS kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
110
|
|
111
|
add_test(NAME kind_fmcad08_large_CEX_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
112
|
COMMAND bash -c "tail -n +8 ${L}.xml > ${L}_tailed2.xml"
|
113
|
WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${L}/
|
114
|
)
|
115
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
116
|
PROPERTIES REQUIRED_FILES ${L}.xml
|
117
|
DEPENDS kind_fmcad08_large_CEX_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
118
|
|
119
|
|
120
|
add_test(NAME kind_fmcad08_large_CEX_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
121
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_tailed1.xml ../${L}_tailed2.xml
|
122
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
123
|
)
|
124
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
125
|
PROPERTIES REQUIRED_FILES ${L}_tailed1.xml
|
126
|
DEPENDS kind_fmcad08_large_CEX_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
127
|
|
128
|
|
129
|
if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class)
|
130
|
#message("add tests for comaring Zustre and lustrec in large/src/CEX")
|
131
|
add_test(NAME kind_fmcad08_large_CEX_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
132
|
COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ XPathParser_lusi ${ZUSTRE_NODE_OPT} ../${L}.lusi ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
133
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
134
|
)
|
135
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
136
|
PROPERTIES REQUIRED_FILES ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi
|
137
|
DEPENDS kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT} )
|
138
|
|
139
|
set(LUSTRE_NODE_OPT "top")
|
140
|
# First command generate C files from Lustre file
|
141
|
Lustre_Compile(LUS_FILE ${lus_file}
|
142
|
NODE ${LUSTRE_NODE_OPT}
|
143
|
OPTS ""
|
144
|
DIR ${ZUSTRE_OUTPUT_DIR})
|
145
|
|
146
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
147
|
add_test(NAME kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
148
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
|
149
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
150
|
)
|
151
|
|
152
|
#********************* make -f ${L}.makefile ***************************
|
153
|
add_test(NAME kind_fmcad08_large_CEX_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
154
|
COMMAND make -f ${L}.makefile
|
155
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
156
|
)
|
157
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
158
|
PROPERTIES DEPENDS kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
159
|
REQUIRED_FILES ${L}.makefile
|
160
|
)
|
161
|
|
162
|
#************** execute C binary **********************************
|
163
|
|
164
|
if (BASH)
|
165
|
add_test(
|
166
|
NAME kind_fmcad08_large_CEX_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
167
|
COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
|
168
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
169
|
)
|
170
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
171
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
|
172
|
DEPENDS kind_fmcad08_large_CEX_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
|
173
|
else()
|
174
|
message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
|
175
|
endif()
|
176
|
|
177
|
#************** execute C binary **********************************
|
178
|
add_test(NAME kind_fmcad08_large_CEX_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
179
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ZUSTRE_output_values
|
180
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
181
|
)
|
182
|
SET_TESTS_PROPERTIES ( kind_fmcad08_large_CEX_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
183
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
|
184
|
DEPENDS kind_fmcad08_large_CEX_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
|
185
|
|
186
|
|
187
|
|
188
|
endif()
|
189
|
|
190
|
ENDFOREACH()
|
191
|
add_custom_target(kind_fmcad08_large_CEX COMMAND ${CMAKE_CTEST_COMMAND} -R kind_fmcad08_large_CEX)
|
192
|
|