Relax disjoint check for globals and fresh pointers. #1858

andreistefanescu · 2023-04-18T13:02:56Z

No description provided.

RyanGlScott · 2023-04-18T13:04:48Z

What is the motivation behind this patch? Can you provide an example of where this check does the wrong thing with its previous behavior?

RyanGlScott

This looks reasonable at a quick glance. I like the fact that the code is more consistent with the treatment of fresh pointers in enforceDisjointAllocSpec.

A couple of minor suggestions inline.

intTests/test_llvm_global_fresh_pointer/test.bc

intTests/test_llvm_global_fresh_pointer/test.saw

Relax disjoint check for globals and fresh pointers.

f1ea76b

andreistefanescu requested review from chameco and RyanGlScott April 18, 2023 13:03

Add test.

96e0204

RyanGlScott reviewed Apr 18, 2023

View reviewed changes

intTests/test_llvm_global_fresh_pointer/test.bc Outdated Show resolved Hide resolved

intTests/test_llvm_global_fresh_pointer/test.saw Show resolved Hide resolved

Address comments.

ab8a473

andreistefanescu requested a review from RyanGlScott April 18, 2023 14:08

RyanGlScott approved these changes Apr 18, 2023

View reviewed changes

andreistefanescu merged commit fad48d8 into master Apr 19, 2023

mergify bot deleted the fix-disjoint-global branch April 19, 2023 01:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Relax disjoint check for globals and fresh pointers. #1858

Relax disjoint check for globals and fresh pointers. #1858

andreistefanescu commented Apr 18, 2023

RyanGlScott commented Apr 18, 2023

RyanGlScott left a comment

Relax disjoint check for globals and fresh pointers. #1858

Relax disjoint check for globals and fresh pointers. #1858

Conversation

andreistefanescu commented Apr 18, 2023

RyanGlScott commented Apr 18, 2023

RyanGlScott left a comment

Choose a reason for hiding this comment