diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-04-06 13:27:19 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-04-06 13:27:19 +0100 |
commit | 9be2bcd27db2e78cec1a47bd2eec3e731c0bf352 (patch) | |
tree | 56bdac32d8ce292d895aebeadcd341abf404b029 | |
parent | b53684a200816f84772a5627932d700a5eda1b97 (diff) |
Added basic lit configuration file for running tests.
-rw-r--r-- | Test/lit.site.cfg | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg new file mode 100644 index 00000000..575f310b --- /dev/null +++ b/Test/lit.site.cfg @@ -0,0 +1,100 @@ +# -*- 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' + +# 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 )) |