search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Gitignore for portfolio #88

Closed radl97 closed 3 years ago

radl97 commented 3 years ago

Executing Portfolio test created a file that is not ignored by git.

It seems that the file test/portfolio/0 is supposed to be a logfile of some kind. Maybe this file is created in test/portfolio/ instead of inside test/portfolio/Output?

AdamZsofi commented 3 years ago

I saw that 0 before a few times, but I thought it disappeared with another small fix. Can you share the command (or one of the commands) used? I'll try to reproduce the problem and take a look at it.

radl97 commented 3 years ago

I just ran make check-functional and then it showed up in git status. Working in master branch, even tested with GAZER_TOOLS_DIR=$PWD/build/tools/ lit test/portfolio/.

Note: The test fails for me, probably because LLVM9 was not properly installed, maybe that triggers the bug.

EDIT: grammar

AdamZsofi commented 3 years ago

There was a typo, when creating the logfile (I tried blaming perl-tidy for it, but I couldn't reproduce the thing, so it was probably my fault), which instead of concatenating the filename, tried to divide two strings, but instead of dying it returned 0.

Patched it on the branch portfolio-patch, but there is a good chance, that I'll need to patch a few other things in the coming days, so I'll merge and close this afterwards.