blob: 4997e83688915b82c0bbcb1435c4a404fd989875 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
# -*- Python -*-
# Configuration file for the 'lit' test runner.
import os
import sys
import re
import platform
import lit.util
import lit.formats
# name: The name of this test suite.
config.name = 'Boogie'
config.test_format = lit.formats.ShTest(execute_external=False)
# suffixes: A list of file extensions to treat as test files. This is overriden
# by individual lit.local.cfg files in the test subdirectories.
config.suffixes = ['.bpl']
# excludes: A list of directories to exclude from the testsuite. The 'Inputs'
# subdirectories contain auxiliary inputs for various tests in their parent
# directories.
config.excludes = []
# test_source_root: The root path where tests are located.
config.test_source_root = os.path.dirname(os.path.abspath(__file__))
# test_exec_root: The root path where tests should be run.
config.test_exec_root = config.test_source_root
# Propagate 'HOME' through the environment.
if 'HOME' in os.environ:
config.environment['HOME'] = os.environ['HOME']
# Propagate 'INCLUDE' through the environment.
if 'INCLUDE' in os.environ:
config.environment['INCLUDE'] = os.environ['INCLUDE']
# Propagate 'LIB' through the environment.
if 'LIB' in os.environ:
config.environment['LIB'] = os.environ['LIB']
# Propagate the temp directory. Windows requires this because it uses \Windows\
# if none of these are present.
if 'TMP' in os.environ:
config.environment['TMP'] = os.environ['TMP']
if 'TEMP' in os.environ:
config.environment['TEMP'] = os.environ['TEMP']
# Propagate PYTHON_EXECUTABLE into the environment
config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', '')
# Check that the object root is known.
if config.test_exec_root is None:
lit_config.fatal('Could not determine execution root for tests!')
### Add Boogie specific substitutions
# Find Boogie.exe
up = os.path.dirname
repositoryRoot = up(
up( os.path.abspath(__file__) )
)
lit_config.note('Repository root is {}'.format(repositoryRoot))
boogieExecutable = os.path.join( repositoryRoot,
'Binaries',
'Boogie.exe'
)
if not os.path.exists(boogieExecutable):
lit_config.fatal('Could not find Boogie.exe at {}'.format(boogieExecutable))
if os.name == 'posix':
boogieExecutable = 'mono ' + boogieExecutable
# Expected output does not contain logo
boogieExecutable += ' -nologo'
# We do not want absolute or relative paths in error messages, just the basename of the file
boogieExecutable += ' -useBaseNameForFileName'
# Allow user to provide extra arguments to Boogie
boogieParams = lit_config.params.get('boogie_params','')
if len(boogieParams) > 0:
boogieExecutable = boogieExecutable + ' ' + boogieParams
# Inform user what executable is being used
lit_config.note('Using Boogie: {}\n'.format(boogieExecutable))
config.substitutions.append( ('%boogie', boogieExecutable) )
# Add diff tool substitution
diffExecutable = None
if os.name == 'posix':
diffExecutable = 'diff --unified=3'
elif os.name == 'nt':
diffExecutable = 'fc'
else:
lit_config.fatal('Unsupported platform')
config.substitutions.append( ('%diff', diffExecutable ))
|
