Repository navigation

Develop - #88

Open

hbgit wants to merge 281 commits into

masterfrom

develop

Open

Develop#88
hbgit wants to merge 281 commits into
masterfrom
develop

This pull request is big! We're only showing the most recent 250 commits

Commits on Aug 12, 2026
Commits on Aug 13, 2026
Commits on Aug 16, 2026
- fix(klee): escalate to SIGKILL when a backend overruns its slice
  
  GuilhermeBn198
  and
  claude
  committed
  06f4985
- fix(eval): capture backend output to a file and reap orphaned processes
  
  GuilhermeBn198
  and
  claude
  committed
  041bb61
- feat(juliet): model rand()/srand() as nondeterministic over [0, RAND_MAX]
  
  GuilhermeBn198
  and
  claude
  committed
  cfbf900
- feat(juliet): stratify sampling by test family instead of by filename prefix
  
  GuilhermeBn198
  and
  claude
  committed
  50f8dd9
- feat(eval): add a storage watchdog for unattended baseline runs
  
  GuilhermeBn198
  and
  claude
  committed
  f7175c3
- docs: add the v5 baseline report and the defect-reduction plan
  
  GuilhermeBn198
  and
  claude
  committed
  b93cc54
- refactor: move the Juliet harness to tests/juliet/ and untrack test-comp2026
  
  GuilhermeBn198
  and
  claude
  committed
  045c97f
- docs: plan Test-Comp conformance and review the Crab-LLVM dependency
  
  GuilhermeBn198
  and
  claude
  committed
  8606a7e
- docs: plan the --add-invariants revival via Clam dev16
  
  GuilhermeBn198
  and
  claude
  committed
  82e8161
- docs(plans): fix the installed binary path and declare v5 comparability
  
  GuilhermeBn198
  and
  claude
  committed
  bad55b8
- fix(invariants): refuse --add-invariants instead of ignoring it
  
  GuilhermeBn198
  and
  claude
  committed
  1a8c6a3
- feat(invariants): bring --add-invariants back on Clam dev16
  
  GuilhermeBn198
  and
  claude
  committed
  6f806fe
- feat(test-comp): emit a Test-Comp test suite, and fix the three bugs that made it impossible
  
  GuilhermeBn198
  and
  claude
  committed
  231ce71
- chore: ignore the unit-test build tree
  
  GuilhermeBn198
  and
  claude
  committed
  8a4de91
- ci: gate on TestCov reproducing the emitted test suites
  
  GuilhermeBn198
  and
  claude
  committed
  11934bb
- docs(testcomp): record the falsifiability check, and what it exposed
  
  GuilhermeBn198
  and
  claude
  committed
  ea10a2b
- ci: fire on feat/** branches, for pushes and for stacked PRs
  
  GuilhermeBn198
  and
  claude
  committed
  9da09d4
- ci: cover feature branches via pull_request only, not also via push
  
  GuilhermeBn198
  and
  claude
  committed
  d37521a
- fix(testcomp): keep the KEEP_WORK notice off stdout
  
  GuilhermeBn198
  and
  claude
  committed
  80383b5
- docs: investigate finding K, and add a progress checklist
  
  GuilhermeBn198
  and
  claude
  committed
  3be786c
Commits on Aug 17, 2026
Commits on Aug 22, 2026
- Merge pull request #57 from hbgit/feat/castle-juliet-baseline
  GuilhermeBn198
  authored
  49954ad
- fix(docker): build Clam with clang-16, and gate Dockerfile.dev on PRs
  
  GuilhermeBn198
  and
  claude
  committed
  247e577
- Merge pull request #58 from hbgit/fix/clam-image-build
  GuilhermeBn198
  authored
  1c46d9f
- chore(docker): pin Clam and its three dependencies to SHAs
  
  GuilhermeBn198
  and
  claude
  committed
  b35e536
- Merge pull request #59 from hbgit/chore/pin-clam-shas
  GuilhermeBn198
  authored
  05a5535
- fix(reachability): announce a target that is never called (finding B)
  
  GuilhermeBn198
  and
  claude
  committed
  3526ae5
- Merge pull request #60 from hbgit/fix/target-coverage-warning
  GuilhermeBn198
  authored
  e1438e5
- feat(testcomp): BenchExec packaging, and always emit a test suite (H1.4)
  
  GuilhermeBn198
  and
  claude
  committed
  69329c2
- fix(nondet-log): unsigned rows carried a duplicated value column
  
  GuilhermeBn198
  and
  claude
  committed
  705417a
- Merge pull request #61 from hbgit/feat/testcomp-benchexec-packaging
  GuilhermeBn198
  authored
  bb64de7
- Merge pull request #62 from hbgit/fix/nondet-log-unsigned-row
  GuilhermeBn198
  authored
  35233a1
- fix(klee): name symbolic objects by their type, not by unexpanded macro text
  
  GuilhermeBn198
  and
  claude
  committed
  087cc9e
- feat(testcomp): Cover-Branches suites from KLEE's own path vectors
  
  GuilhermeBn198
  and
  claude
  committed
  6e1288e
- fix(testcomp): stop labelling TestCov's Result line as a coverage claim
  
  GuilhermeBn198
  and
  claude
  committed
  376e31b
- docs(testcomp): record how to read the 2026-08-22 corpus results
  
  GuilhermeBn198
  and
  claude
  committed
  d6da0e9
- docs: H1.3 and H2.5 done — Cover-Branches lands via KLEE's ktest output
  
  GuilhermeBn198
  and
  claude
  committed
  381aeae
- fix(testcomp): nested sampling and a category-interleaved manifest; quota 150
  
  GuilhermeBn198
  and
  claude
  committed
  67b8378
Commits on Aug 23, 2026
Commits on Aug 24, 2026
- test(testcomp): make v11 a 2x2 factorial with its own control
  
  GuilhermeBn198
  and
  claude
  committed
  75f2a0a
- Merge pull request #64 from hbgit/feat/cover-branches
  GuilhermeBn198
  authored
  120b986
- fix(assume): the XCSP family spells it "assume", and spelling was the bug
  
  GuilhermeBn198
  and
  claude
  committed
  ce26f01
- fix(slice): give the criterion function back its body before linking
  
  GuilhermeBn198
  and
  claude
  committed
  57a0d12
- fix(verdict): do not report FAILED for a violation nothing can reproduce
  
  GuilhermeBn198
  and
  claude
  committed
  621db93
- test: chain the v12 regression sweep and the v13 guard measurement
  
  GuilhermeBn198
  and
  claude
  committed
  8472427
- fix(budget): always reach a verdict, and always flush it
  
  GuilhermeBn198
  and
  claude
  committed
  a377611
- test: point the chained measurement at v14
  
  GuilhermeBn198
  and
  claude
  committed
  43f245a
- fix(slice): bound the slicer too
  
  GuilhermeBn198
  and
  claude
  committed
  336dc06
- test: run v14 at the competition budget, with CASTLE and Juliet beside it
  
  GuilhermeBn198
  and
  claude
  committed
  b81780f
- test: build the v14 paper run -- 4939 tasks at the competition budget
  
  GuilhermeBn198
  and
  claude
  committed
  241adb2
- test: 72h deadline, and six shards for the half that needs them
  
  GuilhermeBn198
  and
  claude
  committed
  bf77658
Commits on Aug 25, 2026
- fix(klee): --max-time takes integer seconds, and a fraction kills the run
  
  GuilhermeBn198
  and
  claude
  committed
  e9129dd
- test: relaunch the paper run on v15, gated behind its own validation
  
  GuilhermeBn198
  and
  claude
  committed
  fae19a0
Commits on Aug 27, 2026
- docs(v15): the paper run's report, and stop versioning campaign results
  
  GuilhermeBn198
  and
  claude
  committed
  3c24375
- chore: campaign results out of the repository
  
  GuilhermeBn198
  and
  claude
  committed
  475454b
Commits on Sep 1, 2026
- fix: address timeout and fuzzer review feedback
  
  Copilot
  and
  hbgit
  authored
  54cb6d5
- fix: preserve timeout budget headroom
  
  Copilot
  and
  hbgit
  authored
  fa285b1
- fix: report fuzzer availability errors
  
  Copilot
  and
  hbgit
  authored
  6d044eb
- Merge pull request #65 from hbgit/fix/slice-target-stub
  hbgit
  authored
  4150327
Commits on Sep 26, 2026
- docs(tacasv1): design spec — replace LibFuzzer with AFL++
  GuilhermeBn198
  committed
  b72835b
- docs(tacasv1): implementation plan — LibFuzzer to AFL++
  GuilhermeBn198
  committed
  e98397d
- feat(tacasv1): install AFL++ 4.40c (PCGUARD) in the dev image
  GuilhermeBn198
  committed
  fdd1fb4
- feat(tacasv1): resolve afl-clang-fast/afl-fuzz paths
  GuilhermeBn198
  committed
  0031130
- feat(tacasv1): replace FindLibFuzzer with FindAFLPlusPlus
  GuilhermeBn198
  committed
  1455be8
- feat(tacasv1): AFL++ persistent nondet generator
  GuilhermeBn198
  committed
  208c6dc
- feat(tacasv1): drive AFL++ from the Caller
  GuilhermeBn198
  committed
  d9ab6d0
- feat(tacasv1): --nondet-generator afl replaces fuzzer
  GuilhermeBn198
  committed
  c18cd77
- chore(tacasv1): rename SKIP_LIB_FUZZER→SKIP_AFL_PLUS_PLUS and update docs
  GuilhermeBn198
  committed
  abae549
- fix(tacasv1): make the AFL++ arm build and confirm violations
  
  GuilhermeBn198
  and
  claude
  committed
  87f9aaa
- fix(tacasv1): address the review of the AFL++ fix commit
  
  GuilhermeBn198
  and
  claude
  committed
  d089c90
- feat(tacasv1): CmpLog companion binary, and rewind the AFL++ read index
  
  GuilhermeBn198
  and
  claude
  committed
  1a49aa5
- fix(tacasv1): bound afl-fuzz by timeout alone, not also by -V
  
  GuilhermeBn198
  and
  claude
  committed
  a6068c6
- fix(verdict): an empty vector is a witness when the program reads no input
  
  GuilhermeBn198
  and
  claude
  committed
  6c7b0f2
Commits on Sep 27, 2026
- docs(tacasv2a): design spec — slicing for reach/assert that keeps the suite valid
  
  GuilhermeBn198
  and
  claude
  committed
  a12ac9b
- docs(tacasv2a): implementation plan
  
  GuilhermeBn198
  and
  claude
  committed
  83ec67c
- feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics
  
  GuilhermeBn198
  and
  claude
  committed
  74ecf4a
- fix(tacasv2a): slice without cutoff and keep every nondet read
  
  GuilhermeBn198
  and
  claude
  committed
  336a26d
- feat(tacasv2a): --slice in assert mode
  
  GuilhermeBn198
  and
  claude
  committed
  c36a532
- docs(tacasv2a): diagnostic sample re-run on the implementation
  
  GuilhermeBn198
  and
  claude
  committed
  75bdefd
- fix(tacasv2a): take the nondet names from the program as well
  
  GuilhermeBn198
  and
  claude
  committed
  ffad3e5
- ci: run the PR gates on PRs stacked on tacas/** branches
  
  GuilhermeBn198
  and
  claude
  committed
  0b0e855
- Revert "ci: run the PR gates on PRs stacked on tacas/** branches"
  
  GuilhermeBn198
  and
  claude
  committed
  8eb66b3
- test(tacasv1): the evaluation runner's fuzzer arm is GENERATOR=afl
  
  GuilhermeBn198
  and
  claude
  committed
  5a4e2fb
- Merge branch 'feat/tacas-aflpp' into feat/tacas-slicing
  GuilhermeBn198
  committed
  d182b20
- docs(tacas): experiment log -- one entry per mini-round (R1-R6)
  
  GuilhermeBn198
  and
  claude
  committed
  2d6bf1a
- docs(tacasv2b): design spec — slicing for memtrack/memcleanup after instrumentation
  
  GuilhermeBn198
  and
  claude
  committed
  bb0afa3
- docs(tacasv2b): implementation plan
  
  GuilhermeBn198
  and
  claude
  committed
  e8e244e
- feat(tacasv2b): runtime names as slicing criteria
  
  GuilhermeBn198
  and
  claude
  committed
  e4ac339
- feat(tacasv2b): --slice for memtrack and memcleanup, after instrumentation
  
  GuilhermeBn198
  and
  claude
  committed
  8864d7c
- test(tacasv2b): SV-COMP MemSafety evaluation harness
  
  GuilhermeBn198
  and
  claude
  committed
  9632286
- test(tacasv2b): opt-in flags for the CASTLE and Juliet runners
  
  GuilhermeBn198
  and
  claude
  committed
  2cddf6b
- docs(tacas): R7 -- overflow slicing probe
  
  GuilhermeBn198
  and
  claude
  committed
  e29e45d
- docs(tacasv2c): study and draft spec -- slicing for overflow
  
  GuilhermeBn198
  and
  claude
  committed
  5836a44
- docs(tacasv2c): implementation plan
  
  GuilhermeBn198
  and
  claude
  committed
  7b9f0eb
- feat(tacasv2c): --slice for overflow
  
  GuilhermeBn198
  and
  claude
  committed
  4eb6ba4
- test(tacasv2c): NoOverflows harness
  
  GuilhermeBn198
  and
  claude
  committed
  31d3fc6
- docs(tacas): R8-R9 -- memory slicing rounds, wrong TRUE found
  
  GuilhermeBn198
  and
  claude
  committed
  aa76cee
- fix(tacasv2b): external calls are slicing criteria after instrumentation
  
  GuilhermeBn198
  and
  claude
  committed
  96e078f
- Merge branch 'feat/tacas-slicing-mem' into feat/tacas-slicing-overflow
  GuilhermeBn198
  committed
  4d4a4cf
- fix(verdict): KLEE halting on its timer is a timeout, not a proof
  
  GuilhermeBn198
  and
  claude
  committed
  30f2215
- Merge branch 'feat/tacas-slicing-mem' into feat/tacas-slicing-overflow
  GuilhermeBn198
  committed
  3ec37a9
- docs(tacas): R9b-R13 and the two correctness defects they exposed
  
  GuilhermeBn198
  and
  claude
  committed
  e6b9296
- docs(tacas): sleep-3 is a pre-existing memtrack false positive, not slicing
  
  GuilhermeBn198
  and
  claude
  committed
  4d1954f
Commits on Sep 28, 2026
Commits on Sep 29, 2026
- docs(tacasv3a): design spec -- smart seeds plumbing (AFL++ <-> KLEE)
  
  GuilhermeBn198
  and
  claude
  committed
  56d11d1
- docs(tacasv3a): implementation plan
  
  GuilhermeBn198
  and
  claude
  committed
  1f68143
- feat(tacasv3a): pure seed-store helpers
  
  GuilhermeBn198
  and
  claude
  committed
  fb8248a
- feat(tacasv3a): a seed store that survives the hybrid's phases
  
  GuilhermeBn198
  and
  claude
  committed
  a560d1e
- feat(tacasv3a): the fuzzer corpus reaches KLEE as typed seeds
  
  GuilhermeBn198
  and
  claude
  committed
  b662546
- fix(tacasv3a): bound and phase-gate the replays, clean store, keep proofs
  
  GuilhermeBn198
  and
  claude
  committed
  3a89b46
- docs(tacas): R15 -- Cover-Error sample, tacasv2 x v15
  
  GuilhermeBn198
  and
  claude
  committed
  3096644
- docs(tacas): R15 -- Cover-Branches sample
  
  GuilhermeBn198
  and
  claude
  committed
  14c8506
- fix(verdict): the program's abort() prunes the path, it does not end the search
  
  GuilhermeBn198
  and
  claude
  committed
  1eb8a30
- docs(tacas): R18 partial and the 2026-09-29 handoff
  
  GuilhermeBn198
  and
  claude
  committed
  3b156aa
- docs(tacas): R18 -- the abort fix clears 6 of 8 wrong TRUEs
  
  GuilhermeBn198
  and
  claude
  committed
  4206581
- docs(tacas): drop the stale R18 partial from the handoff
  
  GuilhermeBn198
  and
  claude
  committed
  6fa1b24
- fix(verdict): KLEE finishing after dropping paths is not a proof
  
  GuilhermeBn198
  and
  claude
  committed
  4c16013
- docs(tacas): R16 -- the seed exchange covers 148 vs 129
  
  GuilhermeBn198
  and
  claude
  committed
  0e6e015
- fix(verdict): a path an assumption pruned is not a dropped path
  
  GuilhermeBn198
  and
  claude
  committed
  7c6f892
- fix(verdict): a KLEE that died, or hit its memory cap, proved nothing
  
  GuilhermeBn198
  and
  claude
  committed
  09d8066
- feat(slice): slice once per run, and experiment knobs for the slice
  
  GuilhermeBn198
  and
  claude
  committed
  93e8de3
- fix(slice): bound the post-slice cleanup like the slicer
  
  GuilhermeBn198
  and
  claude
  committed
  be6754d
Commits on Sep 30, 2026
- perf(slice): scan the IR for names without std::regex
  
  GuilhermeBn198
  and
  claude
  committed
  8cdcb07
- fix(afl): the fuzzer's input runs out as zeros, not as a replay of itself
  
  GuilhermeBn198
  and
  claude
  committed
  c3d2bbe
- feat(hybrid): --alternate-engines, turns that end when an engine stagnates
  
  GuilhermeBn198
  and
  claude
  committed
  4d1e91e
- docs(schedule): phases 2 and 3 as the TACAS line delivered them
  
  GuilhermeBn198
  and
  claude
  committed
  2e931ba
- fix(hybrid): the review of --alternate-engines
  
  GuilhermeBn198
  and
  claude
  committed
  902eaf5
- fix(hybrid): the fuzzer gets all of KLEE's vectors, built once, with growing patience
  
  GuilhermeBn198
  and
  claude
  committed
  e247b64
- fix(afl): one build budget for the three AFL++ binaries
  
  GuilhermeBn198
  and
  claude
  committed
  ca996ba
- fix(memtrack): check memset/memcpy/memmove under LLVM 16's opaque pointers
  
  GuilhermeBn198
  and
  claude
  committed
  956df7b
- docs(tacas): handoff after 2d, 3b and the review fixes
  
  GuilhermeBn198
  and
  claude
  committed
  8111145
- fix(afl): a fuzzer binary that fails to link says so, and why
  
  GuilhermeBn198
  and
  claude
  committed
  56e1cb9
- feat(seeds): the fuzzer entries that reached new edges go to KLEE first
  
  GuilhermeBn198
  and
  claude
  committed
  b664ae6
- docs(tacas): handoff -- 3c v1 and R20
  
  GuilhermeBn198
  and
  claude
  committed
  9853308
- docs(tacas): R16 -- Cover-Branches, the seed exchange 49.7% vs 47.7%
  
  GuilhermeBn198
  and
  claude
  committed
  6e7bfdd
- docs(tacas): R17 and a partial R19
  
  GuilhermeBn198
  and
  claude
  committed
  caf30b6
- fix(eval): a crash replayed from the fuzzer is not a tool failure
  
  GuilhermeBn198
  and
  claude
  committed
  e482c3a
- fix(memtrack): check the strings a %s or puts will read
  
  GuilhermeBn198
  and
  claude
  committed
  e3a2500
- fix(memtrack): the %s checks behind MAP2CHECK_CHECK_CSTRINGS=1
  
  GuilhermeBn198
  and
  claude
  committed
  f18be77
- feat(suite): the fuzzer's corpus in the Cover-Branches suite (knob)
  
  GuilhermeBn198
  and
  claude
  committed
  d6da7c5
- docs(tacas): handoff -- strings, fuzzer suite, R21/R22
  
  GuilhermeBn198
  and
  claude
  committed
  d89ef22
- docs(tacas): R17 complete, and why the alternation lost eca-* tasks
  
  GuilhermeBn198
  and
  claude
  committed
  fd83c46
- docs(tacas): handoff -- R23 and the alternation fix
  
  GuilhermeBn198
  and
  claude
  committed
  f1f5237
- feat(hybrid): run KLEE's vectors on natively, completed with zeros
  
  GuilhermeBn198
  and
  claude
  committed
  7636ec5
- docs(tacas): handoff -- vector replay and R24
  
  GuilhermeBn198
  and
  claude
  committed
  54c5d58
- fix(eval): the programs under test must not inherit the manifest
  
  GuilhermeBn198
  and
  claude
  committed
  65a9286
- docs(tacas): R19 and R21 results
  
  GuilhermeBn198
  and
  claude
  committed
  e972dc4
- docs(tacas): handoff -- night state
  
  GuilhermeBn198
  and
  claude
  committed
  4f02611
- fix(frontend): an unreadable input program is an error that says so
  
  GuilhermeBn198
  and
  claude
  committed
  49efa33
- docs(tacas): handoff -- R22 rerun
  
  GuilhermeBn198
  and
  claude
  committed
  c312c7a
- docs(tacas): handoff -- the Crab-LLVM to Clam gap is the next front
  
  GuilhermeBn198
  and
  claude
  committed
  e265f5e
- docs(tacas): handoff -- first probe of the old crab-llvm engine vs Clam
  
  GuilhermeBn198
  and
  claude
  committed
  4fabab4
- docs(tacas): INV-1 -- the old crab-llvm vs Clam, and where the gain really was
  
  GuilhermeBn198
  and
  claude
  committed
  dff7246
- feat(invariants): Clam profiles, an invariant count, and SSA pre-optimization
  
  GuilhermeBn198
  and
  claude
  committed
  35f32c9
- docs(tacas): handoff -- INV-1 and R25
  
  GuilhermeBn198
  and
  claude
  committed
  51dc7f0
- docs(tacas): first results of R20, R22, R23 and R24
  
  GuilhermeBn198
  and
  claude
  committed
  811fc13
- chore(release): Map2Check 9.0.0
  
  GuilhermeBn198
  and
  claude
  committed
  fdd6bd9
- docs(tacas): R21 CASTLE, and the scheduler's collapsed tab fields
  
  GuilhermeBn198
  and
  claude
  committed
  a17aca5
- docs(tacas): R20 and R23 seeds complete
  
  GuilhermeBn198
  and
  claude
  committed
  c3ebf40
- fix(invariants): bound Clam like the slicer
  
  GuilhermeBn198
  and
  claude
  committed
  a1506bc
- docs(tacas): overnight results -- R22, R23, R24, R25
  
  GuilhermeBn198
  and
  claude
  committed
  e80a478
- feat(hybrid): the alternation and the fuzzer suite become the 9.0 defaults
  
  GuilhermeBn198
  and
  claude
  committed
  e8fe0da
- docs: campaign plan on the 2765-task Cover-Branches set, witness study in the backlog
  
  GuilhermeBn198
  and
  claude
  committed
  3476ff7
- docs(tacas): handoff -- the 9.0 campaign is chained after R26
  
  GuilhermeBn198
  and
  claude
  committed
  529d43a
Commits on Oct 1, 2026
- docs(tacas): R26 complete and the first batches of the 9.0 campaign
  
  GuilhermeBn198
  and
  claude
  committed
  b1f1870
Commits on Oct 2, 2026
- docs(tacas): handoff -- resuming the 9.0 campaign after a power loss
  
  GuilhermeBn198
  and
  claude
  committed
  a65377e
Commits on Oct 3, 2026
- fix(hybrid): link the fuzzer with libm, and kill a KLEE an interrupt cannot stop
  
  GuilhermeBn198
  and
  claude
  committed
  76eedfc
- docs(tacas): the two defects of the 9.0 campaign and the build swap
  
  GuilhermeBn198
  and
  claude
  committed
  43ee04e
- docs(tacas): 9.0 campaign -- Cover-Error, CASTLE and Juliet a/b/d complete
  
  GuilhermeBn198
  and
  claude
  committed
  c8a4f6a
Commits on Oct 4, 2026
- docs(tacas): handoff -- Cover-Branches shard 5 split in four
  
  GuilhermeBn198
  and
  claude
  committed
  60597d7
- docs(backlog): campaign sample vs the official Test-Comp 2026 set; assume-pruned KLEE paths
  
  GuilhermeBn198
  and
  claude
  committed
  b51ee3d
Commits on Oct 5, 2026
- docs(tacas): 9.0 campaign -- Cover-Branches complete
  
  GuilhermeBn198
  and
  claude
  committed
  7c08270
- fix(klee): end an assumption-pruned path with _exit, so KLEE writes its test
  
  GuilhermeBn198
  and
  claude
  committed
  e4e0b74
- fix(suite): assumption-pruned paths give way to deeper ones in a capped suite
  
  GuilhermeBn198
  and
  claude
  committed
  6848d23
Commits on Oct 6, 2026
- docs(tacas): assume-pruned paths fix and its rerun
  
  GuilhermeBn198
  and
  claude
  committed
  53a43e8
- chore: untrack local documents committed by mistake in 53a43e821
  
  GuilhermeBn198
  and
  claude
  committed
  5d57fff
Commits on Oct 7, 2026
Commits on Oct 12, 2026
- fix(testcomp): drop each validator's scratch so a full corpus fits on disk
  
  GuilhermeBn198
  and
  claude
  committed
  4a2dcca
- test(testcomp): let TESTCOV_S=0 skip the internal TestCov
  
  GuilhermeBn198
  and
  claude
  committed
  14766fd
- test(testcomp): official corpora with proportional stratification
  
  GuilhermeBn198
  and
  claude
  committed
  0149e22
- docs(tacas): official Test-Comp environment and the V99 campaign handoff
  
  GuilhermeBn198
  and
  claude
  committed
  3e0dcef
- fix(nondet): model float, longlong, ulonglong, u8/u16/u32 and nondet_memory
  
  GuilhermeBn198
  and
  claude
  committed
  05a1573
- docs(tacas): issue #74 fix, probe and the V99 re-run of the affected categories
  
  GuilhermeBn198
  and
  claude
  committed
  5146272
- docs(tacas): issue #74 re-run report and the KLEE log explosion (#75)
  
  GuilhermeBn198
  and
  claude
  committed
  a2a164a
Commits on Oct 13, 2026
- docs(changelog): unmodeled nondet types (#74) and the official Test-Comp validation
  
  GuilhermeBn198
  and
  claude
  committed
  4855cbb
- fix(runtime): stop the KLEE nondet log from exploding the error path
  
  GuilhermeBn198
  and
  claude
  committed
  8da5794
- feat(klee): MAP2CHECK_KLEE_MAX_MEMORY knob; changelog for #75
  
  GuilhermeBn198
  and
  claude
  committed
  b4bda90
- docs(tacas): issue #75 probes and the 40-task CE sample on install_v99c
  
  GuilhermeBn198
  and
  claude
  committed
  a2fbc56
Commits on Oct 15, 2026
- test(testcomp): loop_reads.c is COVERED since #75
  
  GuilhermeBn198
  and
  claude
  committed
  0b149ce
Commits on Oct 22, 2026
- fix(frontend): read every nondet type of klee_log.csv
  
  Guilherme Bernardo
  and
  claude
  committed
  7db6dd5
- fix(nondet): redirect calls to an existing runtime name instead of renaming
  
  Guilherme Bernardo
  and
  claude
  committed
  9c14229
- fix(counterexample): the C testcase falls back to the violating .ktest
  
  Guilherme Bernardo
  and
  claude
  committed
  c2bcc6c
- fix(memtrack): GNU %m consumes no printf argument
  
  Guilherme Bernardo
  and
  claude
  committed
  223194e
- fix(tests): a tool crash after the fuzzer phase is ERROR
  
  Guilherme Bernardo
  and
  claude
  committed
  b25e6af
- fix(testcomp): make-archive.sh resolves its paths before changing directory
  
  Guilherme Bernardo
  and
  claude
  committed
  deea32a
- docs(testcomp): the test-suite format and how each corpus manifest was built
  
  Guilherme Bernardo
  and
  claude
  committed
  fb2423b
Commits on Oct 23, 2026
- Merge pull request #73 from hbgit/feat/map2check-9.0
  hbgit
  authored
  064a666
Commits on Oct 24, 2026
- feat(testcomp): smoke test, README and licenses in the Test-Comp archive
  
  authored and
  GuilhermeBn198
  committed
  e455680
- fix(testcomp): complete the archive's license notices; enforce them
  
  Guilherme Bernardo
  and
  claude
  committed
  28e14ef
- Merge pull request #85 from hbgit/feat/testcomp27-archive
  GuilhermeBn198
  authored
  c59e8cd
- fix(testcomp): the archive's AFL++ phase needs gcc-multilib on the host
  
  GuilhermeBn198
  and
  claude
  committed
  7609c3b
- Merge pull request #86 from hbgit/fix/testcomp27-archive-toolchain
  GuilhermeBn198
  authored
  4186227
- fix(testcomp): the smoke test requires evidence that each engine ran
  
  GuilhermeBn198
  and
  claude
  committed
  2ee2a0d
Commits on Oct 25, 2026
- Merge pull request #87 from hbgit/fix/testcomp27-engine-evidence
  hbgit
  authored
  cb5a8f8
Commits on Oct 26, 2026
- Merge remote-tracking branch 'origin/master' into develop
  
  Copilot
  and
  hbgit
  authored
  256321f
- ci: limit greetings workflow token permissions
  
  Copilot
  and
  hbgit
  authored
  3e91452
- test(testcomp): sweep per-task work dirs left by killed runs
  GuilhermeBn198
  committed
  6e3eacb
- feat(testcomp): one wrapper and one tool-info module for SV-COMP and Test-Comp
  GuilhermeBn198
  committed
  9fb3718
- Merge pull request #89 from hbgit/feat/testcomp-unified-wrapper
  GuilhermeBn198
  authored
  0bca42e

Commits

Commits on Aug 12, 2026

Commits on Aug 13, 2026

Commits on Aug 16, 2026

Commits on Aug 17, 2026

Commits on Aug 22, 2026

Commits on Aug 23, 2026

Commits on Aug 24, 2026

Commits on Aug 25, 2026

Commits on Aug 27, 2026

Commits on Sep 1, 2026

Commits on Sep 26, 2026

Commits on Sep 27, 2026