diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-04-06 16:51:21 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-04-06 16:51:21 +0100 |
commit | 480d5908a98a7f3a4c170f2994b240c87bcaf567 (patch) | |
tree | 31aec8374be377b1a57e0c382fed5d7910e8c87c | |
parent | 71f8c1bb366154083ff5eff5943520d9511ea014 (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.
-rw-r--r-- | Test/lit.site.cfg | 3 |
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: |