Add --wide-pointer-encoding: 192-bit pointers with flat addresses#8954

Draft

tautschnig wants to merge 27 commits intodiffblue:developfrom

tautschnig:feature/wide-pointer-encoding

Commits on Apr 8, 2026

MiniSat: add set_limit_incremental_simplification

tautschnig
and
kiro-agent
committed
Fix CaDiCaL l_get crash for var_no 0

tautschnig
and
kiro-agent
committed
Add --wide-pointer-encoding to bv_pointerst

tautschnig
and
kiro-agent
committed
Add alternative test descriptor for wide pointer encoding

tautschnig
and
kiro-agent
committed
Address-based pointer equality and comparison (fixes #8200, #8161)

tautschnig
and
kiro-agent
committed
Defer I2P backward constraints to finish_eager_conversion

tautschnig
and
kiro-agent
committed
Add object_base_address expression and encoding infrastructure

tautschnig
and
kiro-agent
committed
Fix boolbv_widtht for wide pointer encoding

tautschnig
and
kiro-agent
committed
Fix byte-level pointer representation for wide encoding

tautschnig
and
kiro-agent
committed
Add --model-stack-layout for stack growth and adjacent placement

tautschnig
and
kiro-agent
committed
Fix #2117: address reuse after free with wide pointer encoding

tautschnig
and
kiro-agent
committed
Optimize backward I2P constraints for performance

tautschnig
and
kiro-agent
committed
Add regression test for #8200: cast-to-pointer

tautschnig
and
kiro-agent
committed
Add regression test for #8161: inconsistent pointer comparison

tautschnig
and
kiro-agent
committed
Add regression test for #8103: I2P dereference

tautschnig
and
kiro-agent
committed
Add regression test for #2117: address reuse after free

tautschnig
and
kiro-agent
committed
Add regression test for --model-stack-layout

tautschnig
and
kiro-agent
committed
Fix Pointer_comparison3 wide descriptor: expect 13 failures, not 11

tautschnig
and
kiro-agent
committed
Add documentation for wide pointer encoding

tautschnig
and
kiro-agent
committed
Integrate backward I2P refinement into bv_refinementt::check_SAT

tautschnig
and
kiro-agent
committed
Fix simplifier dynamic object detection for malloc_may_alias

tautschnig
and
kiro-agent
committed
Refine value_set_dereference comment for pointer-containing types

tautschnig
and
kiro-agent
committed
Fix crashes and correctness: boolbv_width, byte_extract, backward I2P

tautschnig
and
kiro-agent
committed
Fix havoc_slice/test_struct_raw_bytes descriptor: expect 11 failures

tautschnig
and
kiro-agent
committed
Add wide-pointer-encoding descriptors for Malloc10, Malloc14, null8

tautschnig
and
kiro-agent
committed
Tag tests with no-wide-pointer-encoding for different expected results

tautschnig
and
kiro-agent
committed
Fix MiniSat crash: freeze variables from finish_eager_conversion

tautschnig
and
kiro-agent
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add --wide-pointer-encoding: 192-bit pointers with flat addresses#8954

Add --wide-pointer-encoding: 192-bit pointers with flat addresses#8954
tautschnig wants to merge 27 commits intodiffblue:developfrom
tautschnig:feature/wide-pointer-encoding

Commits on Apr 8, 2026

MiniSat: add set_limit_incremental_simplification

Fix CaDiCaL l_get crash for var_no 0

Add --wide-pointer-encoding to bv_pointerst

Add alternative test descriptor for wide pointer encoding

Address-based pointer equality and comparison (fixes #8200, #8161)

Defer I2P backward constraints to finish_eager_conversion

Add object_base_address expression and encoding infrastructure

Fix boolbv_widtht for wide pointer encoding

Fix byte-level pointer representation for wide encoding

Add --model-stack-layout for stack growth and adjacent placement

Fix #2117: address reuse after free with wide pointer encoding

Optimize backward I2P constraints for performance

Add regression test for #8200: cast-to-pointer

Add regression test for #8161: inconsistent pointer comparison

Add regression test for #8103: I2P dereference

Add regression test for #2117: address reuse after free

Add regression test for --model-stack-layout

Fix Pointer_comparison3 wide descriptor: expect 13 failures, not 11

Add documentation for wide pointer encoding

Integrate backward I2P refinement into bv_refinementt::check_SAT

Fix simplifier dynamic object detection for malloc_may_alias

Refine value_set_dereference comment for pointer-containing types

Fix crashes and correctness: boolbv_width, byte_extract, backward I2P

Fix havoc_slice/test_struct_raw_bytes descriptor: expect 11 failures

Add wide-pointer-encoding descriptors for Malloc10, Malloc14, null8

Tag tests with no-wide-pointer-encoding for different expected results

Fix MiniSat crash: freeze variables from finish_eager_conversion