Repository navigation
Conversation
Crab-LLVM (FindCrabLlvm.cmake / seahorn/crab-llvm) was never wired into the modern CMake build, so --add-invariants pointed at a missing bin/crabllvm/bin/crabllvm.py and broke the pipeline. Detect the absence of the binary and compile normally with a warning instead of failing.
caller.cpp unconditionally passed -m2c-entry-function to opt, but that cl::opt is registered only by MemoryTrackPass. In overflow/assert/ reachability modes (which don't load MemoryTrackPass) opt aborted on the unknown argument, so main was never renamed to __map2check_main__ and the fuzzer/KLEE link failed with 'undefined reference to __map2check_main__' (the 'timeout: failed to run command ... No such file or directory' noise in the eval output). Gate the flag on the memtrack/memcleanup modes.
The verdict parser matched 'timeout: failed to run command ... No such file or directory' (the coreutils timeout error emitted when the fuzzer binary is missing) as a TIMEOUT. A real timeout is signalled by map2check's 'Forcing timeout' message. detect_verdict/classify_verdict now check FALSE -> TRUE -> 'Forcing timeout' (TIMEOUT) -> infra-failure patterns (ERROR) -> UNKNOWN, and the runners report an ERROR bucket.
The -m2c-entry-function bug (caller.cpp passing the flag to opt even when MemoryTrackPass was not loaded) made --check-overflow, --check-asserts and --target-function abort and report ERROR/UNKNOWN. test_modes.sh exercises each mode with a buggy and a safe program and asserts definitive verdicts, so this class of regression fails CI. Wired into the castle-regression job.
find_row_with_address() cast pointers to unsigned (32-bit), so with KLEE's 1024 GiB heap two distinct live allocations that share the low 32 bits collided in the allocation log, corrupting tracking and producing false positives (safe swap-trick double-free/use-after-free cases 415-7/8, 416-7/8/10) and latent false negatives in any multi-allocation program. Use unsigned long, consistent with the long addr field.
AssertPass only matched __VERIFIER_assert, so C programs using the standard C assert() (lowered to __assert_fail by clang) were never checked and the --check-asserts mode returned ERROR. Match __assert_fail and emit map2check_assert(0, line, function) using its operands. Adds a libc-assert case to test_modes.sh.
- Mark 134 (format string), 253 (return-value check), 362 (race) as out of scope: no Map2Check mode detects them. - Re-map 369 (divide by zero) to --check-overflow (OverflowPass instruments sdiv; detection still pending divisionByZeroError()). - Extract the violation line from 'map2check_property line N' instead of the first 'line \d+' match, which was matching LibFuzzer's 'inline 8-bit counters' and reporting 'line 8' for every case.
…he op
OperationsFunctions.hpp declared map2check_binop_{add,sub,mul,sdiv} with i64
params while AnalysisModeOverflow.c defines them with int (i32), so the
runtime overflow check was silently broken (overflow only surfaced via
clang's -Winteger-overflow warning). Declare i32 and pass operands without
the i64 cast. Also insert the runtime check BEFORE the arithmetic op:
a division by zero traps (SIGFPE) in the op itself, so a check inserted
after it would never run.
Implement divisionByZeroError() (previously a no-op) to report a dedicated FALSE-DIVBYZERO property instead of folding it into overflow, matching the convention of KLEE (DivisionByZero), CBMC (--div-by-zero-check) and SV-COMP (CWE-369 uses unreach-call, not no-overflow). Adds the property end-to-end: backend enum, write_property, frontend enum + string parse + display, eval parsers, and div_bug/div_safe cases in test_modes.sh.
OverflowPass declared the binop checkers with i64 operands while the runtime took int, so the check read garbage. The previous fix aligned both at i32, which traded one bug for another: every long/long long operation then skipped instrumentation entirely, and Juliet CWE190/191 has plenty of those. Neither width is right on its own. SV-COMP defines no-overflow over "the resulting type of an operation", so an i32 add that wraps must be reported as such -- widening its operands to 64 bits makes it stop overflowing and masks the bug -- while an i64 add that wraps must be reported too. So the operands are sign-extended to a common i64 ABI (lossless) and the operation's own bit width rides along as an extra argument, with the runtime range-checking the exact result against that width. One symbol per operation rather than one per width, which is how UBSan's __ubsan_handle_*_overflow handlers carry the operand type. Also fixed while rewriting the runtime checks: - sub delegated to add(param1, -param2), which is itself UB at INT_MIN and wrong for the boundary cases it was meant to catch. - mul's hand-rolled limit arithmetic evaluated INT_MIN / param1 before ruling out param1 == -1. - sdiv's overflow test was `(a == MIN || b == MIN) && (a == -1 || b == -1)`, which both missed MIN / -1 in one direction and fired on safe divisions in the other. It is now `a == MIN && b == -1`. - SRem was an empty case in the pass, so `x % 0` went unchecked entirely -- a CWE-369 gap, since division by zero covers the modulo operator too. The predicates are cross-checked against __builtin_*_overflow at widths 8/16/32/64 for every op. test_modes.sh (already wired into CI) grows cases for long long add/mul overflow, INT_MIN / -1, and modulo by zero, each of which fails against the previous build: 16 passed, 0 failed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The scope list stopped at CWE-190, so integer underflow (191) and divide by zero (369) were never exercised even though both map to --check-overflow and both are what the width-aware binop fix changes. Juliet ships 1794 and 468 self-contained cases for them respectively. The existing LIMIT counts across every CWE and then breaks out of the whole run, so a truncated pass spends its entire budget inside whichever CWE comes first and the rest go unmeasured. LIMIT_PER_CWE caps each CWE instead, which is what a balanced sample needs. JULIET_CWES overrides the scope list for targeted slices. find's output is now sorted, so a truncated run is a reproducible prefix rather than whatever order the filesystem returned. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
map2check's default is hybrid: LibFuzzer for 0.2x the budget, then KLEE for the rest. map2check.cpp prints "Note: Forcing timeout" whenever a phase exhausts its slice, which the fuzzer phase does on essentially every run that does not get an early hit -- it is the normal path into KLEE, not a verdict. Both evaluation runners keyed TIMEOUT off that string. Since FALSE and TRUE were tested first, the damage landed entirely on the runs that could not be decided: every UNKNOWN and every ERROR came out labelled TIMEOUT. A bucket that reads "just needs more time" was absorbing real tool failures. Caught on CWE190_Integer_Overflow__char_fscanf_add_01: KLEE segfaults on the __isoc99_fscanf external, map2check recovers and reports UNKNOWN, and the run was recorded as a 13-second TIMEOUT. It now reports ERROR, which is the actionable signal. The trustworthy timeout signals are the harness's own -- the outer `timeout` exiting 124, or a run that consumed its budget without deciding -- so both runners now capture the exit code they were discarding with `|| true` and pass it, along with elapsed time and the budget, to the classifier. Second mislabelling found alongside it: the ERROR pattern matched "undefined reference", but KLEE prints "KLEE: WARNING: undefined reference to function: fscanf" on healthy runs for every unresolved external. The pattern was meant for the linker error, so it now skips KLEE's warning lines -- otherwise removing the "Forcing timeout" branch would have simply moved those runs from TIMEOUT to ERROR. The two runners carried separate copies of this logic and both had the same bug, so it now lives in tests/lib/verdict_classifier.sh with tests/integration/test_verdict_classifier.sh covering every rule (20 cases, 3 of which fail against the previous logic). Wired into CI. Both runners also persist each run's raw output now. The verdict alone cannot be re-derived from the CSV, so this bug meant discarding the in-flight baseline and starting over; next time a reclassification will do. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both backends are launched under `timeout <slice>` with no --kill-after. KLEE installs a SIGTERM handler to shut down gracefully, but that handler never runs while the solver is wedged: `timeout` sends the signal, KLEE catches and ignores it, and `timeout` then waits forever on a child that will not die. The whole run hangs past its own budget. Measured on a Juliet CWE-190 fscanf case, which stalled for 18 minutes on a 60s budget. Process state at the time: timeout 48 .../klee ... <- still alive, 2m10s of CPU klee <- SigCgt has bit 14 set: SIGTERM caught, ignored With `timeout -k 10` the same case completes in 13s. LibFuzzer gets the same treatment: -jobs=8 forks workers that must not outlive the budget either. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The evaluation harnesses read map2check's output through `$( )`, which
deadlocks. Command substitution reads its pipe until EOF, and EOF only
arrives once every write end closes. map2check spawns KLEE and LibFuzzer as
grandchildren that inherit that pipe; when the outer `timeout` kills
map2check, they are orphaned but keep the write end open, and the harness
blocks forever.
Observed directly on a run stalled 18 minutes on its first file:
pipe:[472046]
pid=113 fd=3 <- harness subshell, blocked reading
pid=48538 fd=2 <- orphaned `timeout 48 klee`, write end held
pid=48539 fd=2 <- orphaned klee, write end held
map2check itself was already gone.
run_isolated redirects to a file instead, so nothing waits on a pipe, and
reaps every process whose cwd is inside the run's private temp directory --
`timeout` only signals its direct child, so KLEE would otherwise keep
burning CPU for the rest of the suite. Verified against a grandchild that
traps SIGTERM and outlives its parent: rc=124, no survivors.
The private cwd also fixes two pre-existing hazards in the CASTLE runner,
whose cwd was the repo root: map2check names its scratch by SHA-1 of the
input bitcode (caller.cpp:63), so pass 1 and the --add-invariants pass
collided on one directory, and a directory orphaned by an aborted run was
reused by the next run of the same input.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…MAX] Juliet routes its random inputs through std_testcase.h macros that expand inside each testcase, so rand() itself is the only interception point. Left unstubbed, rand() is an unresolved external: KLEE calls the real libc function and gets ONE concrete value. The program then has a single feasible path and map2check answers VERIFICATION SUCCEEDED -- not UNKNOWN, but a confident wrong TRUE. All 6 CWE190 int_rand_add false negatives in the v3 baseline were this. int_rand_square escaped only by luck: data*data overflows for |data| > 46340, so almost any concrete draw trips it, while int_rand_add needs data == INT_MAX exactly. Modelling an unknown external as nondeterministic is a sound over-approximation and the standard SV-COMP treatment; the concrete-value alternative is the unsound one. The range is constrained rather than left open, because that is where a naive stub creates false positives: rand() returns [0, RAND_MAX] and URAND31() depends on it, so an unconstrained int would hand the solver negative draws real rand() cannot produce. A static assert enforces that RAND_MAX+1 is a power of two, so the mask stays exact or the build fails loudly instead of silently biasing the input space. Verified on the known false negative: bad => VERIFICATION FAILED (was SUCCEEDED), good => VERIFICATION SUCCEEDED (no new false positive). Also records two known biases in the header so they are not mistaken for results: decodeHexChars returning 0 can turn a real bug into a trivially safe program, and printLine() as a no-op stops reading the buffer, which could mask an out-of-bounds read whose only sink is the print (1924 CWE121 testcases call printLine(data); zero do in CWE190/191/369). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… prefix LIMIT_PER_CWE took the first N files in alphabetical order. A Juliet family owns ~26 consecutive filenames, so 60 files collapsed into 2-3 families. Measured coverage of the previous baseline: CWE-190: 6 of 90 families (6.7%) CWE-191: 5 of 69 families (7.2%) CWE-369: 2 of 18 families (11.1%) The consequences were not subtle. Every int64_t family went untested, so the width-aware i64 overflow work the baseline existed to validate was never exercised once. In CWE-369 only float families were reached -- float division by zero yields IEEE infinity and is not undefined behaviour at all -- so every genuine integer divide-by-zero was missed. The resulting "0% recall on CWE-369" measured the sampler, not the tool. PER_FAMILY samples every family instead. Three per family is the default, justified by the previous run's data: grouping its rows by (family, variant) gave 26 groups and all 26 were perfectly homogeneous, with short_min_multiply covering 25 of its 26 flow variants and never disagreeing with itself. The three files are spread across the variant range rather than taken from the front: variants _01.._09 are the simple control-flow shapes and the hard ones live in the _1x/_2x range, so a prefix would reintroduce at the variant level the exact bias being removed at the family level. LIMIT_PER_CWE now aborts if set to a value that would have capped anything, so the bias cannot return by habit; 0 was the inert "unlimited" default and is still accepted. tests/integration/test_juliet_sampling.sh locks the invariants whose violation would repeat this silently -- a wrong sampler produces plausible output, which is why it went unnoticed across two full runs. The two assertions that execute the runner are sandboxed so the suite needs neither the 570MB Juliet submodule nor a working clang, and an assertion verifies nothing is written into the working tree. 18 tests, 0.2s. This commit also wires the runner to run_isolated (see previous commit). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A full scope-C run is hours long and unattended, and a disk that fills mid-write corrupts the CSV it was writing. Stopping is recoverable because both runners resume from their CSV; a truncated CSV is not. The watchdog samples free space, docker usage, results size, container log size and liveness every five minutes, and halts the run if free space falls under a floor. It reports container log sizes so a missing --log-opt rotation is visible rather than silent: docker's json-file driver is unbounded by default. Docker usage comes from `docker system df` rather than `du /var/lib/docker`, which needs root and silently under-reports without it -- a quietly wrong monitoring number is worse than none, which is the whole failure mode this script exists to prevent. Also fixes .gitignore, where an append landed on the previous line because the file did not end in a newline, breaking both patterns. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Full scope-C evaluation, 2,742 cases, run to completion: CASTLE 217/217 that compile, and Juliet at 421 of 421 families with PER_FAMILY=3. CASTLE precision 98.2% recall 74.0% undecided 16.7% Juliet precision 90.8% recall 46.8% undecided 28.0% Every false positive was traced to its raw output and its source, and the headline is that 33 of the 36 are correct answers to the wrong question. They all report FALSE-MEMTRACK on programs Juliet labels safe, and Juliet's CWE-416 good variants leak by construction -- goodG2B() mallocs and never frees, and says so in a comment. The harness maps CWE-416 to --memtrack, which checks leaks too. Excluding them, Juliet precision is 99.2%; the sole CASTLE false positive found its bug and only misreported the line, so real CASTLE precision is 100%. The 3 genuine false positives are all int64_t_rand_square good variants, where KLEE silently concretizes the imaxabs/sqrtl guard over a now-symbolic input and loses the constraint. Reported as a cost of the rand() fix, which converted 6 false negatives into true positives and introduced these 3. 98% of the 345 timeouts come from two sources: fscanf (242) and listen_socket (96). The same axis explains the false negatives -- input sources fgets, connect_socket, console and environment sit on exactly 50.0% correct among decided cases, the signature of proving the safe variant and missing the vulnerable one every time. The plan prioritises by measured cost: unresolved externals account for 575 lost cases across 887 that take input that way, which is larger than everything else combined. The undecided cluster in CWE-121/122 (252 cases) is filed as an investigation, not a fix -- the obvious hypothesis was tested and rejected, since 100% of UNKNOWN cases log an unresolved reference but so do 87% of decided ones. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…omp2026 The two benchmark harnesses now share one layout. CASTLE already lived in tests/castle/ with its benchmark as a submodule; Juliet's runner sat under test-comp2026/simulation/ purely for historical reasons. test-comp2026/simulation/run_juliet_evaluation.sh -> tests/juliet/run_juliet_evaluation.sh test-comp2026/simulation/juliet_stubs.c -> tests/juliet/juliet_stubs.c test-comp2026/juliet (submodule) -> tests/juliet/juliet-test-suite-c test-comp2026/ is a local workspace for Test-Comp preparation and paper material, so it is untracked and ignored from here on. The files stay on disk; only the tracking stops. Note this does not remove them from the history of master or develop, where they have been since before this branch. Two things were rescued rather than dropped: - README.md cited test-comp2026/.../juliet_wasm/wasm_results.csv as the evidence that the WASM pipeline detects all 15 seeded Juliet bugs. The file is 16 lines; it moves to docs/reports/wasm-juliet-validation.csv so the claim keeps its evidence instead of pointing at an untracked path. - test_wasm_pipeline.sh and test_wasm_entrypoint.sh defaulted MAP2CHECK_PATH to test-comp2026/simulation/release. CI always overrides it, so this was never exercised there, but it would have become a dead path for anyone running locally. Now defaults to install_e2e, which is what CI actually passes. Paths updated in the runner (JULIET_DIR, RESULTS_DIR, the tests/lib sources), in test_juliet_sampling.sh, and in baseline_watchdog.sh. RESULTS_DIR now defaults to tests/juliet/results, mirroring tests/castle/results. Verified after the move: shell syntax on all five touched scripts, the classifier (20) and sampling (18) suites, and an end-to-end run of the relocated runner on CWE-415 -- 6 TP, 6 TN, 0 compile failures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three documents, none of them changing behaviour yet. The Crab-LLVM review answers a question the issue #54 report left open: whether --add-invariants is worth reviving. It is. crab-llvm was renamed to Clam, not abandoned -- upstream pushed nine days ago, branch dev16 targets LLVM 16 explicitly, and the symbol our NonDetPass keys off (verifier.assume) is preserved. Exactly one flag was renamed. Our fork has been stale since 2019 and pins LLVM 6, which is the whole of the breakage. The review also records a hazard that decides the recommendation: an unsound invariant does not produce an error, it produces a wrong TRUE. Under KLEE it prunes a reachable state; under LibFuzzer nondet_assume calls pthread_exit and the execution dies in silence. With 35% of baseline cases taking input through unresolved externals, how Crab models those decides soundness. Hence: fix the silence now, and gate the port behind a CMake flag that is off until a differential run proves no detection is lost. The two implementation plans cover the conformance work that the development plan calls bloqueante. The emitter plan turned out smaller than its 2 pw estimate: the runtime already logs every nondet value in consumption order and flushes it for both engines (NonDetLog.c:17), and the frontend already parses that CSV. What is missing is serialization, so H1.2 collapses into H1.1. The plan is explicit that this covers Cover-Error only -- map2check_exit flushes once per process, so Cover-Branches needs per-input logs and stays out of scope. The TestCov plan makes the official validator a blocking check. Its corpus carries a negative control and an expected-results manifest, so the gate fails in both directions and cannot quietly become vacuous. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase A makes the missing capability loud on every input path; Phase B brings it back behind -DENABLE_CLAM=ON and promotes it only on differential evidence. The flag stays in all three call sites that request it today. They fail until Clam lands, which is the point: a request the tool cannot satisfy is the signal that should be visible, and withdrawing it would recreate exactly the silence issue #54 describes. One carve-out, for data integrity rather than for the flag -- CASTLE's pass 2 replaces pass 1's verdict, so an unhandled exit 3 would write ERROR over a legitimate UNKNOWN and corrupt the CSV instead of failing visibly. Recorded while investigating: because the flag was ignored on the .bc path, that second pass has been a byte-identical re-run of the first through the whole v5 baseline, burning a second timeout budget and writing used_invariants=yes for runs that used none. The capability test is one file asserting two contracts and printing which it checked, so it passes today in the ABSENT state and starts asserting verifier.assume injection the day the image carries Clam -- progress visible in the CI log rather than a red check nobody watches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The binary installs to the prefix root (CMake: DESTINATION .), not to bin/. Every existing harness uses $MAP2CHECK_DIR/map2check; three plans had invented a bin/ path that would have failed on the first run. Also declares the two harness deltas that cross the v5/v6 boundary, since v5 is now frozen as the 'before' of a before/after comparison: used_invariants changes meaning, and pass 2 stops being a duplicate run. With the attribution rule that follows from it -- the headline v6 run keeps invariants off, or the overflow, timeout, sampling and invariant fixes all become jointly uncreditable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase A of the Clam revival. The flag was accepted and silently ignored whenever the input was bitcode -- which is how every baseline run, the CASTLE harness and both BenchExec wrappers invoke the tool. The guard that was meant to warn lived inside `if (!is_llvmir_in)`, so the .bc path skipped it entirely and left no trace at all. map2check now refuses the run with a distinct exit code (3, ERROR_UNAVAILABLE_CAPABILITY) that separates "you typed it wrong" from "this binary cannot do that". The check sits in main() next to the other option validation, not in map2check_execution(), for two reasons: main() is the only place whose return becomes the process exit code, and it runs once instead of once per generator on the hybrid path. That second point surfaced a separate defect, filed as finding G rather than fixed here: main() discards map2check_execution()'s return value at all three call sites, so the exit code never reflects the analysis outcome -- the `return 1` behind --expected-result is swallowed too. The three call sites keep requesting invariants. They fail until Clam lands, which is the point: withdrawing the request would hide the gap and recreate exactly the silence this commit removes. One carve-out, for data integrity rather than for the flag -- CASTLE's pass 2 REPLACES pass 1's verdict, so an unhandled exit 3 would write ERROR over a legitimate UNKNOWN and corrupt the CSV instead of failing visibly. It now recognises exit 3, keeps pass 1's verdict, and records used_invariants=unavailable. Recorded in the findings report: because the flag was ignored on the .bc path, that second pass has been a byte-identical re-run of the first through the whole v5 baseline -- a second full timeout budget per UNKNOWN row, written down as used_invariants=yes for runs that used none. No published verdict changes; the column's meaning and the run times do. The test asserts two contracts and prints which one it checked. Today it reports CAPABILITY: ABSENT and asserts the refusal is loud, names the flag, explains itself and offers the remedy. Once the image carries Clam it will report PRESENT and instead assert that verifier.assume is really injected -- so the flag cannot come back as a no-op wearing a success exit code. No red check is parked in CI: one that is expected to be red gets ignored, and then nobody notices the day it turns green. Verified in the map2check-dev container: 5/5 on the new test, and 56/56 on the existing suite (verdict classifier 20, Juliet sampling 18, main argv 2, modes 16). clang-format deviations unchanged at 79, all pre-existing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Phase B. crab-llvm was renamed to Clam, not abandoned: branch dev16 pins CLAM_LLVM_VERSION 16, upstream pushed nine days ago, and the symbol NonDetPass keys off (verifier.assume) is preserved. Our fork had been stale since 2019 and pinned LLVM 6. The flag list is measured, not translated, and that measurement found a second bug underneath the first. Counting verifier.assume calls in the emitted bitcode on a loop program, against the legacy invocation: baseline (track=num, inter, opt=add-invariants, loc=block-entry) 5 + --crab-promote-assume 1 + --llvm-pp-loops 0 --llvm-pp-loops annihilates injection outright, and --crab-promote-assume rewrites verifier.assume into the llvm.assume intrinsic -- precisely the symbol NonDetPass.cpp:95 matches on, so promoting makes the invariants invisible to Map2Check. Both were in the legacy command line. The capability was dead twice over: even if crab-llvm had still built, it would have injected nothing Map2Check could see. Traced end to end on the fixed invocation: -compiled.bc (Clam output) verifier.assume=5 crab_assume=0 -output.bc (after NonDetPass) verifier.assume=0 crab_assume=5 -result.bc (linked) verifier.assume=0 crab_assume=5 so Clam -> verifier.assume -> map2check_crab_assume -> klee_assume is live from end to end. Off by default (-DENABLE_CLAM=ON), because an unsound invariant does not raise an error: under KLEE klee_assume prunes a reachable state, under LibFuzzer nondet_assume calls pthread_exit and the execution vanishes. Both read as "program is safe". Promotion to default waits on the differential run. Dockerfile.dev builds Clam into /opt/clam and then FAILS THE IMAGE BUILD if a probe program comes back with zero injected assumes -- a silent zero is exactly what hid this for years. libzstd-dev is required rather than optional: LLVM 16 from apt.llvm.org exports zstd::libzstd_shared, so find_package(LLVM) inside Clam fails without it. No optional Crab domain is enabled; --crab-track=num uses the default interval domain. --debug now keeps the scratch directory. Every intermediate of a run lives there and cleanGarbage() deleted it unconditionally, which made the pipeline impossible to inspect after the fact -- and made the injection assertion above unwritable until now. Retires the LLVM 6 machinery: FindCrabLlvm.cmake (unreferenced, no branch pinned) and build_crabllvm.py (hardcodes /llvm/release/llvm600 and g++-5). Also gitignores local agent material -- ai-memory skill installs, editor agent configs, CLAUDE.md backups and the local Test-Comp planning document -- for the same reason test-comp2026/ is ignored: preparation material, not product. Verified in the container, both capability states green from one test file: ABSENT 5/5 on the default build, PRESENT 2/2 on -DENABLE_CLAM=ON with Clam at CLAM_DIR. Rest of the suite unchanged at 56/56. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…that made it impossible --generate-test-suite writes a Test-Comp exchange-format suite -- metadata.xml plus one testcase-N.xml -- for the violation a run found. The format is https://gitlab.com/sosy-lab/software/test-format; the DTDs and public identifiers are transcribed from that repository, not guessed. Almost none of this was meant to be new code. The runtime already records every nondet value in consumption order and flushes it for both engines (NonDetLog.c), and the frontend already parses that CSV for counterexamples, so the plan was a serializer. Building it surfaced why nobody had noticed the log was broken: three defects that only a symbolic executor can see. 1. Use-after-scope in the nondet log. NONDET_CALL.value held the ADDRESS of the `value` parameter of the map2check_nondet_* wrapper -- a stack slot long dead by the time the log is written at exit. Natively the dead frame usually still held the value, so it looked fine. Under KLEE it was a pointer error inside nondet_log_to_file() itself, killing every state: completed paths = 0, and klee_log.csv came out ZERO BYTES on every symbolic run. No counterexample from KLEE has ever carried input values. Fixed by storing the value inline in a union. A pointer cannot work here even if it pointed into the row: the containers memcpy rows into a reallocated array, so any self-referential pointer is stale after the first append. The TODO asking for exactly this union dates from 2020. 2. map2check_nondet_double tagged its rows UNSIGNED, so every logged floating-point input was printed with %u over four bytes of the mantissa. 3. Every forked KLEE state writes the same klee_log.csv on exit and the last one wins -- and it is never the violating state, which aborts early. With (1) fixed the vector came back as [42, -1] on a program whose only violating path is [42, 7]: a sibling state that took the other branch had overwritten it. The nondet flush is now guarded on the violation flag. With all three fixed the emitter recovers the exact violating vector. Also in this commit: SHA-256 for the <programhash> field, pinned to FIPS 180-4 vectors (Map2Check only had SHA-1, which the format does not accept); --property-file so <specification> is copied verbatim from the property BenchExec passes rather than guessed; --test-suite-dir and --architecture. Scope, stated plainly: one test case per run, because map2check_exit() flushes once per process. That is all Cover-Error needs. Cover-Branches needs many test cases and therefore per-input logs, which is separate work, and no suite is emitted for a TRUE or UNKNOWN verdict yet (gap G4). Deliberately no type= or variable= attributes on <input>: Format.md says that if a variable is named and the sequence does not fit it, "the interpretation is undefined". Bare inputs carry no such risk. Verified in the container: 8/8 ctest (Sha256Test 7, TestSuiteTest 13 are new) and 78/78 integration, including a new 12-assertion emission test that checks well-formedness with a real parser, that programhash equals sha256sum of the program, and that the recovered vector is [42, 7] in that order -- the assertion that would have caught all three bugs above. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
KLEE's 2,000 MB default cap killed states on Intel-TDX tasks. The knob passes --max-memory; raising it to 6,000 MB left the 8-task probe at 0/8, so the default stays. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The TestCov gate is bidirectional and failed on b4bda90 and a2fbc56 with "expected NOT_COVERED, observed COVERED". Concretizing the KLEE nondet log (8da5794) removed the state explosion that kept this four-read program from emitting a vector. Measured at BUDGET=120: install_v99b NOT_COVERED, install_v99c COVERED (2/2). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
KleeLogHelper::getListLogFromCSV() knew the type numbers 0-5 only. For any other -- 6-15 already, and the 16-22 of issue #74 -- it left row.type uninitialized, and generateWitnessFunctionName(), which the witness reads for every edge, fell off the end of a non-void function: undefined behaviour on a violation that involves one of those types (review of #73). KleeLogType now mirrors the runtime's enum NONDET_TYPE, in its order, plus UNKNOWN for any other number or a type column that is not a number; the generator name is a full table that always returns, "" for UNKNOWN. New unit test KleeLogTest. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…naming
The abort() rewrite declares map2check_assume. When the same function also
calls the program's own __VERIFIER_assume, NonDetPass then renamed that
declaration onto the occupied name, and LLVM made it map2check_assume.1, a
symbol the runtime does not define: the native builds failed to link
("undefined reference to `map2check_assume.1'") and a reachable target came
back UNKNOWN (review of #73). Reproduced on install_v99c.
adoptRuntimeName() redirects the calls to the existing function when one of
the same type already has the name, and renames otherwise; the nondet
generators and the Crab assume use it too. The repro now answers FAILED with
the input 42. Integration section 39.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
--generate-testcase built map2check_input_array from klee_log.csv only. Past 1024 nondet reads the KLEE runtime writes no log (issue #75), and an aborted KLEE state writes none either: the array came out empty -- `{}`, not even valid C -- and the testcase replayed nothing (review of #73). It now takes the violating .ktest's vector when the log is empty, as the Test-Comp suite already does, and writes `{0}` when there is nothing at all. Measured on 1100 nondet reads with --nondet-generator symex: install_v99c writes an empty array; this writes the 1100 values. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
With MAP2CHECK_CHECK_CSTRINGS=1 the format parser counted %m (strerror of
errno) as a conversion with an argument, so every argument after it shifted
by one: printf("%m %s %p", buf, &byte) checked the one-byte &byte as the %s
string and reported a FALSE-DEREF on a safe program (review of #73;
reproduced on install_v99c). %m now advances no argument; the * of a width or
precision is still counted. Integration section 36 prints that format in its
safe program.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The classifier ignores crash messages between "Exited fuzzer with" and the next phase: there the core dump is the program under test, replayed on the fuzzer's crash. It also hid a crash of Map2Check itself in that stretch (replay processing, suite generation, cleanup): a run whose outer process died on SIGSEGV was classified UNKNOWN, or TIMEOUT near the budget (review of #73). The outer exit status 139/134 now makes it ERROR before that filter; definitive verdicts keep precedence. Three new classifier cases; the two crash cases fail on the previous classifier. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ectory The final zip runs from inside the staging directory. With a relative output name it created the archive there, and the cleanup deleted it -- after `rm -f "$OUT"` had removed the caller's previous archive; a relative path with a directory failed outright (review of #73). Both arguments are now made absolute first, and a missing output directory is an error up front. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s built Review of #73 asked to document the test-suite format (the assumption-pruned marker in particular) and how cover-branches-3500.tsv was created. - docs/test-suite-format.md: the files, metadata, the order and encoding of the inputs, the assumption-pruned comment and why it is safe for the validators, the size cap and the two sources of the vectors (klee_log.csv with its type numbers, and the violating .ktest). The header of test_suite.hpp, which still said Cover-Branches was future work, now points there. - tests/testcomp/corpus/README.md: the command and commit of every manifest. All eight regenerate byte for byte from sv-benchmarks 7efe28dd2 (checked 2026-10-22). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Map2Check 9.0.0: AFL++ engine, smart seeds, engine alternation, sound TRUE verdicts
What the Test-Comp 2027 submission asks of the Zenodo archive: a smoketest.sh that runs the tool on examples shipped with it (the FM-Tools CI merges the registration only if it exits 0), a README, and a LICENSE that lets anybody reproduce the evaluation. - smoketest.sh runs the wrapper on examples/cover_error.c (the suite must carry the input 42 that reaches reach_error) and on examples/cover_branches.c (the suite must hold a test case); - README with the usage, the bundled components and their licenses; - LICENSE (GPL-2.0), the upstream license texts of what is built from source (KLEE 3.1, AFL++ 4.40c, STP 2.3.4, MiniSat), klee-uclibc's, and the Debian copyright file of every bundled library and LLVM tool. Measured: built from install_v99c (the code of this branch), the smoke test passes on a clean ubuntu:24.04 with python3 only, in 4 s. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Review of #85 (Copilot, Herbert): the license bundle missed notices, and the smoke test masked wrapper failures. Licenses, audited from the sources of the exact versions shipped: - KLEE 3.1 runtime: the notices of the 9 files under another license than KLEE's (8 klee-libc, Freestanding/memcmp.c; BSD), verbatim, and the LLVM license for the UBSan runtime; - AFL++ 4.40c: t1ha and xxHash, compiled into afl-fuzz, verbatim, and the LLVM license for SanitizerCoveragePCGUARD; - STP 2.3.4: LICENSE_COMPONENTS and the texts it names for Bit::Vector (Artistic-1.0-Perl, LGPL-2.0; GPL-2 is LICENSE); - LLVM 16's own LICENSE.TXT, and the Debian copyright of clang's resource headers (libclang-common-16-dev); - the full text of every /usr/share/common-licenses license the bundled Debian copyright files name. licenses/README.md is the checklist: component, version, files, license, texts. make-archive.sh enforces it: every file of the archive must match a row whose license files are present, or the archive is not built (648 files covered; a stray file makes it fail). smoketest.sh now fails on a nonzero wrapper exit, printing the log: the wrapper exits 0 whenever Map2Check ran, so any other status is a failure even with a suite on disk. Checked: the archive builds from the develop code (install of fb2423b) and its smoke test passes on a clean ubuntu:26.04, the FM-Tools CI image. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
feat(testcomp): smoke test, README and licenses in the Test-Comp archive
On a clean Ubuntu 24.04 with only python3, the AFL++ binary of the program failed to link: the bundled clang finds no ld, crt1.o, libc or libgcc. The tool does not stop on it -- it skips the fuzzer, gives the whole budget to KLEE and still writes a suite -- so the smoke test passed and every run in the competition would have been KLEE-only. - README: the host needs python3 and gcc-multilib (linker, C runtime and libgcc for 64 and 32 bits); how the engines alternate and what each property's suite holds. - smoketest.sh: fails unless the log shows AFL++ ran (both examples) and KLEE ran (Cover-Branches); the Cover-Branches budget goes from 30 to 60 s, since 30 left KLEE no window. - examples/cover_error.c: defines reach_error, as sv-benchmarks does; an extern-only declaration does not link natively for AFL++. - the wrapper's docstring named the 8.x suite sources. Checked on the rebuilt archive: the smoke test fails on ubuntu:24.04 with only python3, passes with python3 and gcc-multilib on ubuntu:24.04 and 26.04; TestCov 3.11 (the Test-Comp archive) scores the examples' suites TRUE and 100% branch coverage in LP64 and ILP32. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
fix(testcomp): the archive's AFL++ phase needs gcc-multilib on the host
Review of #86: the "Executing AFL++/Klee with map2check" banners are logged before the engine is launched, so they also appear when it fails to start, and the other engine can still produce the suite the smoke test asks for. With afl-fuzz unable to start, KLEE found Cover-Error's 42 and the check passed. The frontend now logs, after each engine, what the engine itself wrote: - "AFL++ ran: N executions, M inputs in the corpus", from execs_done and corpus_count in afl-fuzz's fuzzer_stats; with no executions, a warning carrying the last lines of fuzzer.output, which the scratch cleanup would otherwise remove; - "KLEE ran: N tests generated", from the .ktest files in klee-last. smoketest.sh requires those lines with a positive count instead of the banners: AFL++ in both examples, KLEE in Cover-Branches. Checked on the archive rebuilt from this branch: the smoke test passes on ubuntu:24.04 and 26.04 with python3 and gcc-multilib, and fails with only python3, with an afl-fuzz that exits at once ("AFL++ did not run", its output in the log) and with a klee that exits at once ("KLEE did not run"). Unit tests: 14/14. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
fix(testcomp): the smoke test requires evidence that each engine ran
Owner
Author
|
@copilot resolve the merge conflicts in this pull request |
There was a problem hiding this comment.
🟡 Changes recommended
One or more issues must be addressed before approval.
4 open issues
What changed in this PR
Updates Map2Check’s verification runtime, AFL++ integration, and competition-oriented validation infrastructure.
Changes:
- Adds Test-Comp suite/hash build integration, nondeterministic-type interfaces, assertion handling, and runtime logging/checking changes.
- Expands unit tests and Test-Comp, CASTLE, and Juliet evaluation resources.
- Updates release packaging and migration documentation while removing obsolete simulation files and paper drafts.
| File | Description |
|---|---|
| utils/testcomp-archive/licenses/STP-2.3.4.LICENSE | Updated as part of this pull request. |
| utils/testcomp-archive/licenses/MiniSat.LICENSE | Updated as part of this pull request. |
| utils/testcomp-archive/examples/coverage-error-call.prp | Updated as part of this pull request. |
| utils/testcomp-archive/examples/coverage-branches.prp | Updated as part of this pull request. |
| utils/testcomp-archive/examples/cover_error.c | Updated as part of this pull request. |
| utils/testcomp-archive/examples/cover_branches.c | Updated as part of this pull request. |
| utils/moduleBenchExec/__init__.py | Updated as part of this pull request. |
| utils/map2check-wrapper.py | Updated as part of this pull request. |
| utils/map2check-wrapper-reg-test.py | Updated as part of this pull request. |
| tests/unit/HelloGTest.cpp | Updated as part of this pull request. |
| tests/unit/frontend/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/backend-library/CMakeLists.txt | Updated as part of this pull request. |
| tests/unit/backend-library/BTreeTest.cpp | Updated as part of this pull request. |
| tests/unit/backend-library/AllocationLogTest.cpp | Updated as part of this pull request. |
| tests/testcomp/programs/unreachable.c | Updated as part of this pull request. |
| tests/testcomp/programs/two_guards.c | Updated as part of this pull request. |
| tests/testcomp/programs/single_int.c | Updated as part of this pull request. |
| tests/testcomp/programs/no_input.c | Updated as part of this pull request. |
| tests/testcomp/programs/loop_reads.c | Updated as part of this pull request. |
| tests/testcomp/programs/char_input.c | Updated as part of this pull request. |
| tests/testcomp/official/init.sh | Updated as part of this pull request. |
| tests/testcomp/official/bench-defs/map2check.xml | Updated as part of this pull request. |
| tests/testcomp/launch-v12.sh | Updated as part of this pull request. |
| tests/testcomp/fetch-benchmarks.sh | Updated as part of this pull request. |
| tests/testcomp/expected.txt | Updated as part of this pull request. |
| tests/testcomp/cover-error-call.prp | Updated as part of this pull request. |
| tests/lib/memsafety_classifier.sh | Updated as part of this pull request. |
| tests/juliet/launch-v15-regression.sh | Updated as part of this pull request. |
| tests/juliet/launch-v12-regression.sh | Updated as part of this pull request. |
| tests/juliet/launch-juliet-cd-later.sh | Updated as part of this pull request. |
| tests/integration/test_wasm_pipeline.sh | Updated as part of this pull request. |
| tests/integration/test_wasm_entrypoint.sh | Updated as part of this pull request. |
| tests/integration/test_memsafety_classifier.sh | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-89-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-843-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-835-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-822-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-798-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-787-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-78-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-770-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-761-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-674-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-628-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-617-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-522-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-476-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-416-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-415-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-401-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-369-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-362-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-327-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-253-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-22-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-190-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-134-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-9.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-8.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-7.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-6.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-5.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-4.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-3.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-2.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-10.yml | Updated as part of this pull request. |
| tests/castle/benchexec/tasks/CASTLE-125-1.yml | Updated as part of this pull request. |
| tests/castle/benchexec/sets/castle-overflow.set | Updated as part of this pull request. |
| tests/castle/benchexec/sets/castle-memcleanup.set | Updated as part of this pull request. |
| tests/castle/benchexec/map2check_castle.xml | Updated as part of this pull request. |
| test-comp2026/simulation/map2check-v8.xml | Updated as part of this pull request. |
| test-comp2026/simulation/map2check-v8-heap.xml | Updated as part of this pull request. |
| test-comp2026/.gitignore | Updated as part of this pull request. |
| scripts/prepare-release.sh | Updated as part of this pull request. |
| scripts/package-release.sh | Updated as part of this pull request. |
| scripts/make-release.sh | Updated as part of this pull request. |
| modules/frontend/utils/sha256.hpp | Updated as part of this pull request. |
| modules/frontend/utils/log.cpp | Updated as part of this pull request. |
| modules/frontend/utils/gen_crypto_hash.cpp | Updated as part of this pull request. |
| modules/frontend/utils/CMakeLists.txt | Updated as part of this pull request. |
| modules/frontend/test_suite/CMakeLists.txt | Updated as part of this pull request. |
| modules/frontend/counter_example/counter_example.hpp | Updated as part of this pull request. |
| modules/frontend/CMakeLists.txt | Updated as part of this pull request. |
| modules/backend/pass/NonDetPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/NonDetFunctions.hpp | Updated as part of this pull request. |
| modules/backend/pass/MemoryTrackPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/AssertPass.hpp | Updated as part of this pull request. |
| modules/backend/pass/AssertPass.cpp | Updated as part of this pull request. |
| modules/backend/library/lib/WitnessGenerationNone.c | Updated as part of this pull request. |
| modules/backend/library/lib/WitnessGeneration.c | Updated as part of this pull request. |
| modules/backend/library/lib/PropertyGenerator.c | Updated as part of this pull request. |
| modules/backend/library/lib/NonDetGeneratorNone.c | Updated as part of this pull request. |
| modules/backend/library/lib/Map2CheckFunctions.c | Updated as part of this pull request. |
| modules/backend/library/lib/ListLog.c | Updated as part of this pull request. |
| modules/backend/library/lib/ContainerBTree.c | Updated as part of this pull request. |
| modules/backend/library/lib/CMakeLists.txt | Updated as part of this pull request. |
| modules/backend/library/lib/BTree.c | Updated as part of this pull request. |
| modules/backend/library/lib/AnalysisModeMemtrack.c | Updated as part of this pull request. |
| modules/backend/library/lib/AnalysisModeMemcleanup.c | Updated as part of this pull request. |
| modules/backend/library/lib/AllocationLog.c | Updated as part of this pull request. |
| modules/backend/library/header/WitnessGeneration.h | Updated as part of this pull request. |
| modules/backend/library/header/NonDetLog.h | Updated as part of this pull request. |
| modules/backend/library/header/NonDetGenerator.h | Updated as part of this pull request. |
| make-unit-test.sh | Updated as part of this pull request. |
| examples/use-after-free/sample_use_after_free.c | Updated as part of this pull request. |
| examples/use-after-free/README.md | Updated as part of this pull request. |
| docs/superpowers/specs/2026-09-29-tacas-3c-seed-ranking-design.md | Updated as part of this pull request. |
| docs/reports/wasm-juliet-validation.csv | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/06-conclusao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/05-demonstracao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/04-ciberseguranca.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/03-arquitetura.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/02-historia.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sections/01-introducao.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/README.md | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig5-cicd.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig4-testcomp2026.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig2-pipeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/img/fig1-timeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/sbseg-article/.gitignore | Updated as part of this pull request. |
| docs/paper-sbseg-2026/references/references.bib | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig5-cicd.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig4-testcomp2026.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig3-passes.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig2-pipeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/figures/fig1-timeline.mmd | Updated as part of this pull request. |
| docs/paper-sbseg-2026/appendix/reprodutibilidade.md | Updated as part of this pull request. |
| docs/map2check_migration_plan.md | Updated as part of this pull request. |
| cmake/FindCrabLlvm.cmake | Updated as part of this pull request. |
| cmake/FindAFLPlusPlus.cmake | Updated as part of this pull request. |
| .gitmodules | Updated as part of this pull request. |
| .github/workflows/release.yml | Updated as part of this pull request. |
Review effort: Balanced
| <propertyfile>/home/bench/benchexec_files/tests/castle/benchexec/properties/valid-memcleanup.prp</propertyfile> | ||
| </tasks> | ||
|
|
||
| <tasks name="CASTLE-reachability"> |
| * a live allocation. Stops at the first invalid byte (ERROR_DEREF is set and | ||
| * the caller's map2check_check_deref reports it), before reading it. */ | ||
| void map2check_check_cstring(const char *string) { | ||
| if (string == NULL) return; |
Comment on lines
+9
to
+10
| <includesfile>/home/bench/benchexec_files/tests/castle/benchexec/sets/castle-memsafety.set</includesfile> | ||
| <propertyfile>/home/bench/benchexec_files/tests/castle/benchexec/properties/valid-memsafety.prp</propertyfile> |
Comment on lines
+8
to
+14
| int sum = 0; | ||
| for (int i = 0; i < 4; i++) { | ||
| sum += __VERIFIER_nondet_int(); | ||
| } | ||
| if (sum == 10) { | ||
| reach_error(); | ||
| } |
# Conflicts: # .github/workflows/ci.yml # TODO.md # modules/backend/library/lib/NonDetGeneratorKlee.c # modules/backend/library/lib/NonDetGeneratorLibFuzzy.c # modules/backend/library/lib/NonDetLog.c # modules/frontend/map2check.cpp # tests/unit/CMakeLists.txt Co-authored-by: hbgit <1494322+hbgit@users.noreply.github.com>
Co-authored-by: hbgit <1494322+hbgit@users.noreply.github.com>
Merged |
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.
feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp
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.
Update for new version.