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
|
endif()
|
59
|
if( ${${L}_zustre_output} MATCHES "<Answer>CEX</Answer>")
|
60
|
#message("${L}.xml is CEX")
|
61
|
set(ZUSTRE_ANSWER_${L} "CEX")
|
62
|
elseif( ${${L}_zustre_output} MATCHES "<Answer>SAFE</Answer>")
|
63
|
#message("${L}.xml is SAFE")
|
64
|
set(ZUSTRE_ANSWER_${L} "SAFE")
|
65
|
elseif( ${${L}_zustre_output} MATCHES "<Answer>TIMEOUT</Answer>")
|
66
|
#message("${L}.xml is TIMEOUT")
|
67
|
set(ZUSTRE_ANSWER_${L} "TIMEOUT")
|
68
|
else()
|
69
|
#message("${L}.xml is Error")
|
70
|
set(ZUSTRE_ANSWER_${L} "ERROR")
|
71
|
endif()
|
72
|
ENDFOREACH()
|
73
|
|
74
|
|
75
|
|
76
|
|
77
|
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
|
78
|
get_filename_component(L ${lus_file} NAME_WE)
|
79
|
set(ZUSTRE_NODE_OPT "top")
|
80
|
|
81
|
Lustre_Compile(LUS_FILE ${lus_file}
|
82
|
NODE ""
|
83
|
OPTS "-horn")
|
84
|
|
85
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
86
|
add_test(NAME kind_fmcad08_memory1_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
|
87
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}}
|
88
|
)
|
89
|
|
90
|
Zustre_Compile(LUS_FILE ${lus_file}
|
91
|
NODE ${ZUSTRE_NODE_OPT}
|
92
|
OPTS ${ZUSTRE_OPTIONS_OPT})
|
93
|
set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
|
94
|
set(ZUSTRE_OUTPUT_DIR ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}})
|
95
|
|
96
|
set(ZUSTRE_ARGS_TEMP "${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}" "> ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml")
|
97
|
JOIN("${ZUSTRE_ARGS_TEMP}" " " ZUSTRE_ARGS)
|
98
|
|
99
|
add_test(NAME kind_fmcad08_memory1_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
100
|
COMMAND bash -c "${ZUSTRE_COMPILER} ${ZUSTRE_ARGS}"
|
101
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
102
|
)
|
103
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
104
|
PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
|
105
|
DEPENDS kind_fmcad08_memory1_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
|
106
|
|
107
|
|
108
|
add_test(NAME kind_fmcad08_memory1_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
109
|
COMMAND bash -c "tail -n +8 ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml > ${L}_tailed1.xml"
|
110
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
111
|
#DEPENDS kind_fmcad08_memory1_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
112
|
)
|
113
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
114
|
PROPERTIES REQUIRED_FILES ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
115
|
DEPENDS kind_fmcad08_memory1_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
116
|
|
117
|
add_test(NAME kind_fmcad08_memory1_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
118
|
COMMAND bash -c "tail -n +8 ${L}.xml > ${L}_tailed2.xml"
|
119
|
WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${L}/
|
120
|
)
|
121
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
122
|
PROPERTIES REQUIRED_FILES ${L}.xml
|
123
|
DEPENDS kind_fmcad08_memory1_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
124
|
|
125
|
|
126
|
add_test(NAME kind_fmcad08_memory1_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
127
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_tailed1.xml ../${L}_tailed2.xml
|
128
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
129
|
)
|
130
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
131
|
PROPERTIES REQUIRED_FILES ${L}_tailed1.xml
|
132
|
DEPENDS kind_fmcad08_memory1_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
|
133
|
|
134
|
|
135
|
if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class AND ${ZUSTRE_ANSWER_${L}} STREQUAL "CEX" AND EXISTS ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi)
|
136
|
#message("add tests for comaring Zustre and lustrec in memory")
|
137
|
add_test(NAME kind_fmcad08_memory1_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
138
|
COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ XPathParser_lusi ${ZUSTRE_NODE_OPT} ../${L}.lusi ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
|
139
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
140
|
)
|
141
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
|
142
|
PROPERTIES REQUIRED_FILES ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi
|
143
|
DEPENDS kind_fmcad08_memory1_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT} )
|
144
|
|
145
|
set(LUSTRE_NODE_OPT "top")
|
146
|
# First command generate C files from Lustre file
|
147
|
Lustre_Compile(LUS_FILE ${lus_file}
|
148
|
NODE ${LUSTRE_NODE_OPT}
|
149
|
OPTS ""
|
150
|
DIR ${ZUSTRE_OUTPUT_DIR})
|
151
|
|
152
|
set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
|
153
|
add_test(NAME kind_fmcad08_memory1_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
154
|
COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
|
155
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
156
|
)
|
157
|
|
158
|
#********************* make -f ${L}.makefile ***************************
|
159
|
add_test(NAME kind_fmcad08_memory1_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
160
|
COMMAND make -f ${L}.makefile
|
161
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
162
|
)
|
163
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
164
|
PROPERTIES DEPENDS kind_fmcad08_memory1_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
165
|
REQUIRED_FILES ${L}.makefile
|
166
|
)
|
167
|
|
168
|
#************** execute C binary **********************************
|
169
|
|
170
|
if (BASH)
|
171
|
add_test(
|
172
|
NAME kind_fmcad08_memory1_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
173
|
COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
|
174
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
175
|
)
|
176
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
177
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
|
178
|
DEPENDS kind_fmcad08_memory1_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
|
179
|
else()
|
180
|
message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
|
181
|
endif()
|
182
|
|
183
|
#************** execute C binary **********************************
|
184
|
add_test(NAME kind_fmcad08_memory1_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
185
|
COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ZUSTRE_output_values
|
186
|
WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
|
187
|
)
|
188
|
SET_TESTS_PROPERTIES ( kind_fmcad08_memory1_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
|
189
|
PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
|
190
|
DEPENDS kind_fmcad08_memory1_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
|
191
|
|
192
|
|
193
|
|
194
|
endif()
|
195
|
|
196
|
ENDFOREACH()
|
197
|
add_custom_target(kind_fmcad08_memory1 COMMAND ${CMAKE_CTEST_COMMAND} -R kind_fmcad08_memory1)
|
198
|
|