Skip to content

Align functionality of Z3 in Python and C++#77

Merged
yuleisui merged 5 commits into
mainfrom
z3mgr-cpp-py-align
Jul 10, 2026
Merged

Align functionality of Z3 in Python and C++#77
yuleisui merged 5 commits into
mainfrom
z3mgr-cpp-py-align

Conversation

@hanyuone

@hanyuone hanyuone commented Jul 8, 2026

Copy link
Copy Markdown
Collaborator

The output of printExprValues in the Python version is slightly different to the one in the C++ version. Previously, the Python version would output something like this:

-----------SVFVar and Value-----------
ObjVar2 (0x2)                  Value: NULL
ObjVar3 (0x3)                  Value: NULL
ObjVar5 (0x5)                  Value: NULL
ObjVar9 (0x9)                  Value: NULL
ObjVar12 (0xc)                 Value: NULL
ObjVar15 (0xf)                 Value: NULL
ValVar0()                      Value: 2
ValVar1()                      Value: 2
ValVar4(main)                  Value: 0x7f000005
ValVar7(cmp)                   Value: 1
ValVar8()                      Value: 3
ValVar11(svf_assert)           Value: 0x7f00000c
ValVar14()                     Value: 0
-----------------------------------------

When in the C++ version, the address next to each ObjVar would be & addressMask, being something like ObjVar2 (0x7f000002). This PR aligns both outputs.

Tested on dryrun cases, confirmed that the outputs for both C++ and Python for printExprValues are the same.

@yuleisui
yuleisui merged commit bfbce20 into main Jul 10, 2026
4 checks passed
@yuleisui
yuleisui deleted the z3mgr-cpp-py-align branch July 13, 2026 09:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants