AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

byval arg & memory(argmem) don't work together #1029

Closed nunoplopes closed 2 months ago

nunoplopes commented 2 months ago
define void @src(ptr byval(i32) %0) {
  %3 = load i32, ptr %0
  ret void
}

define void @tgt(ptr byval(i32) %0) memory(argmem:readwrite) {
  %3 = load i32, ptr %0
  ret void
}

Alive2 marks the load in tgt as UB. https://alive2.llvm.org/ce/z/EVzWBu

from @regehr