Same IR Code, But Verification Fail

[IamYJLee]

I found something I don't understand while looking into the case of ERROR: Source and target don't have the same return domain.
Why did the verification fail?

https://alive2.llvm.org/ce/z/SBacDP

[nunoplopes]

reduced test case:

declare void @use_writeonly(ptr) memory(write)

define void @src() {
  %src = alloca i32, align 4
  %dest = alloca i32, align 4
  call void @use_writeonly(ptr %dest)
  ret void
}

define void @tgt() {
  %src = alloca i32, align 4
  %dest = alloca i32, align 4
  call void @use_writeonly(ptr %dest)
  ret void
}

[IamYJLee]

I would like to try to fix this problem. Could I get some help to do so?

[nunoplopes]

It's hard to give any concrete advise. The bug can be either in state,cpp (addFnCall), in memory.cpp (refinement of input memory for the function), or in pointer.cpp (refinement of input ptrs to the function).

[IamYJLee]

Thank you for advise.
I am trying to fix this problem.
I saw a difference between the source and target in the function domain.

Source :

domain = (or (and |@use_writeonly#ptr!void#ub!7| |@use_writeonly#ptr!void#noreturn!8|)
    (and |@use_writeonly#ptr!void#ub!7|
         (not |@use_writeonly#ptr!void#noreturn!8|)))

Target:

domain = (or (and |@use_writeonly#ptr!void#ub!7|
         (ite (= #b1 ((_ extract 1 1) (blk_kind #b1)))
              (and (= #b01 (blk_kind #b1)) (= #x4 (blk_size #b1)))
              (bvule (blk_size #b1) #x4))
         |@use_writeonly#ptr!void#noreturn!8|)
    (and |@use_writeonly#ptr!void#ub!7|
         (not |@use_writeonly#ptr!void#noreturn!8|)
         (ite (= #b1 ((_ extract 1 1) (blk_kind #b1)))
              (and (= #b01 (blk_kind #b1)) (= #x4 (blk_size #b1)))
              (bvule (blk_size #b1) #x4))))

And if the memory function attribute is removed, this problem does not occur.
So I am debugging the State::addFnCall function.