summaryrefslogtreecommitdiff
path: root/Test/lit.site.cfg
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 16:51:21 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 16:51:21 +0100
commit480d5908a98a7f3a4c170f2994b240c87bcaf567 (patch)
tree31aec8374be377b1a57e0c382fed5d7910e8c87c /Test/lit.site.cfg
parent71f8c1bb366154083ff5eff5943520d9511ea014 (diff)
Pass -useBaseNameForFileName option to Boogie when running tests.
This is needed because the expected test output contains just the basename of the .bpl files in error messages but lit passes an absolute path to Boogie so without this option error messages would contain absolute paths which would cause the tests to fail. Now all the houdini tests pass when driven by lit.
Diffstat (limited to 'Test/lit.site.cfg')
-rw-r--r--Test/lit.site.cfg3
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index 575f310b..4997e836 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -78,6 +78,9 @@ if os.name == 'posix':
# 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: