Repository navigation
feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp - #89
Merged
Merged
Conversation
A task killed by a reboot never reached the rm -rf at the end of the loop, so its mktemp directory stayed in /tmp. Over the V99c campaign a few reboots left 11 GB in one shard container and filled the Windows disk behind the WSL vhdx. Work directories now live under one root per results dir and shard, emptied when the harness starts.
…Test-Comp The BenchExec maintainers asked for Test-Comp support in the existing tool-info module instead of a second one (sosy-lab/benchexec#1352, sosy-lab/benchmarking/fm-tools!1245). So: - utils/map2check-wrapper.py now dispatches on the property file: COVER(...) generates tests and ends with DONE, CHECK(...) verifies as before. It calls map2check by absolute path, passes --data-model to both modes and points map2check at the bundled AFL++ when present. - map2check-testcomp-wrapper.py and moduleBenchExec/map2check_testcomp.py are gone; moduleBenchExec/map2check.py mirrors the updated upstream module (DONE -> RESULT_DONE, --data-model/--budget only for v9+, UnsupportedFeatureException, version without the "v" prefix). - The archive (make-archive.sh, smoketest.sh, README, licenses table), package-release.sh, the bench-def and the tool-info test follow.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Following the review of sosy-lab/benchexec#1352 and fm-tools!1245, Map2Check now has one wrapper and one BenchExec tool-info module for both SV-COMP and Test-Comp.
utils/map2check-wrapper.pydispatches on the property:COVER(...)→ test generation, ends withDONE;CHECK(...)→ verification, as before.map2check-testcomp-wrapper.pyandmoduleBenchExec/map2check_testcomp.pyremoved;moduleBenchExec/map2check.pymirrors the upstream module updated in benchexec#1352.make-archive.sh,smoketest.sh, README, licenses table),package-release.sh, bench-def and the tool-info test updated.test(testcomp): sweep per-task work dirs left by killed runs, which was only on a local branch.Verification
tests/integration/test_benchexec_toolinfo.py: 24/24; BenchExectest_tool_infoon the archive passes.developbuild:smoketest.shpasses on cleanubuntu:26.04andubuntu:24.04(python3 gcc-multilib).simple_2-2andgcd_1: alldone, suites collected,32bitin metadata; TestCov scores the Cover-Error suite.FALSE_OVERFLOW. A trivially safe program endsUNKNOWNafter the full budget, identical with the old wrapper flags, so it is pre-existing and not part of this PR.After merge
Rebuild the archive and publish it under the reserved Zenodo DOI used by fm-tools!1245.