summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 13:27:19 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 13:27:19 +0100
commit9be2bcd27db2e78cec1a47bd2eec3e731c0bf352 (patch)
tree56bdac32d8ce292d895aebeadcd341abf404b029
parentb53684a200816f84772a5627932d700a5eda1b97 (diff)
Added basic lit configuration file for running tests.
-rw-r--r--Test/lit.site.cfg100
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 ))