Project

General

Profile

Download (7.74 KB) Statistics
| Branch: | Tag: | Revision:
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

    
(1-1/40)