Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Problem with benchmark xml definition #8

Open
PavelAndrianov opened this issue Oct 20, 2020 · 3 comments
Open

Problem with benchmark xml definition #8

PavelAndrianov opened this issue Oct 20, 2020 · 3 comments

Comments

@PavelAndrianov
Copy link
Contributor

Benchmark processing script searches 'benchmark.xml' only in a current directory even if I set it up in configuration as "benchmark file". So, for now I have to make a link to it. Seems, the option is just ignored.
@PavelAndrianov
Copy link
Contributor Author

Seems, the problem is due to launch not from tool directory, but why not to cd it automatically?

@vmordan
Copy link
Contributor

vmordan commented Oct 20, 2020

Option "benchmark file" specifies file, which should be executed by benchexec. Thus if you do not launch benchmark (option -l), that option is ignored. Currently there is no option for xml results file

@PavelAndrianov
Copy link
Contributor Author

That is what exactly what I mean. I tried to launch the benchmark_visualizer on our verifier cloud from the deploy directory (with option -l). And it cannot found the benchmark.xml file until manually goes to the tool directory. I found all symlinks there, so, It has been already prepared the directory. The question is why does it not change the directory by itself?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@PavelAndrianov @vmordan