Alloc-free dev#1

Open

CapZTr wants to merge 41 commits intodevelopmentfrom

Commits on May 13, 2025

Alloc-free verification prototype

natgavrilenko
authored and
Tianrui Zheng
committed
Using stack pointer in alloc tests

natgavrilenko
authored and
Tianrui Zheng
committed
Support alloc-free dev (#794)

committed
Init setup
Tianrui Zheng
committed
Add Alloc and MemFree to witness for debugging
Tianrui Zheng
committed
Modified some memory models and tests
Tianrui Zheng
committed
Fix event and relation extraction of alloc-free for witness
Tianrui Zheng
committed
Modify some relation and constraint definitions
Tianrui Zheng
committed
Merge development into this branch
Tianrui Zheng
committed
Remove unnecessary definition
Tianrui Zheng
committed

Commits on May 14, 2025

Clean c11 and rc11
Tianrui Zheng
committed
Modify as comments
Tianrui Zheng
committed

Commits on Jun 26, 2025

Clean code to prepare rebase
Tianrui Zheng
committed
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Tianrui Zheng
committed

Commits on Jul 3, 2025

Fix merging
Tianrui Zheng
committed
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Tianrui Zheng
committed

Commits on Jul 11, 2025

Fix CI tests: Attempt 1
Tianrui Zheng
committed

Commits on Jul 17, 2025

By Natalia: Add Termination event
Tianrui Zheng
committed
Fix CI tests
Tianrui Zheng
committed

Commits on Jul 18, 2025

Fix CI tests
Tianrui Zheng
committed

Commits on Jul 24, 2025

Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Tianrui Zheng
committed
Fix bugs from merge
Tianrui Zheng
committed

Commits on Aug 1, 2025

Add AllocPtrGraph & AllocMemGraph, modify as comments
Tianrui Zheng
committed

Commits on Aug 7, 2025

Reverse vmm.cat
Tianrui Zheng
committed
Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Tianrui Zheng
committed
Fix bugs from merge
Tianrui Zheng
committed
Remove vmm from AllocFreeTest
Tianrui Zheng
committed
Add DI source location for frees
Tianrui Zheng
committed

Commits on Aug 8, 2025

Add MemAlloc & MemFree to witness
Tianrui Zheng
committed
Remove unused imports
Tianrui Zheng
committed

Commits on Aug 14, 2025

Merge remote-tracking branch 'upstream/development' into alloc-free-dev
Tianrui Zheng
committed

Commits on Aug 21, 2025

Make MemAlloc and MemFree extend GenericMemoryEvent
Tianrui Zheng
committed
Remove M tag when copy alloc
Tianrui Zheng
committed

Commits on Aug 22, 2025

Add HeapAlloc
Tianrui Zheng
committed

Commits on Aug 28, 2025

Add HeapAlloc class
Tianrui Zheng
committed

Commits on Aug 29, 2025

Revert to efa54cc18
Tianrui Zheng
committed
Make MemAlloc & MemFree extend AbstractMemoryCoreEvent
Tianrui Zheng
committed
Use LazyEventGraph for loc and allocMem in LazyRelationAnalysis
Tianrui Zheng
committed
Fix EqualityAliasAnalysis
Tianrui Zheng
committed
Fix EqualityAliasAnalysis
Tianrui Zheng
committed
Small change to LazyRelationAnalysis
Tianrui Zheng
committed