| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
spaces.
|
| |
|
|
|
| |
``fc`` tool on windows because it is buggy when tests are run
concurrently.
|
| |
|
|
|
| |
of Valentin Wüstholz because under Windows Boogie looks in
other locations for Z3.
|
| |
|
|
| |
--dump-file-to-check flag to OutputCheck by default to ease debugging
|
| |
|
|
| |
the user's PATH
|
| |
|
|
| |
DOS line endings and whitespace to diff tool.
|
| |
|
|
| |
if solver executables are missing.
|
| |
|
|
|
|
| |
we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.
|
| |
|
|
|
|
|
| |
so that all whitespace (including mismatching line endings due
to DOS vs UNIX) are ignored. This fixes the test1/Arrays.bpl
test under Windows. It's quite suprising this issue didn't
come up earlier.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
Dan Liew