more testing programs (a3989cfe) · Commits · Adéla Štěpková / reverser

tests/programs/assert/branch_call_phi_and_t.ll

0 → 100644

+30 −0

Original line number	Diff line number	Diff line
		define dso_local i32 @plus(i32 %x) #0 {
		entry:
		%res = add i32 %x, 1
		ret i32 %res
		}

		define dso_local i32 @main() #0 {
		entry:
		%x = call i32 @__VERIFIER_nondet_i32()
		%is_even = and i32 %x, 1
		%cond = trunc i32 %is_even to i1
		br i1 %cond, label %even, label %odd

		even:
		br label %merge

		odd:
		%v2 = call i32 @plus(i32 %x)
		br label %merge

		merge:
		%res = phi i32 [ %x, %even ], [ %v2, %odd ]
		%check = trunc i32 %res to i1
		call void @assert(i1 noundef %check)
		ret i32 0
		}

		declare void @assert(i1 noundef) #1

		declare i32 @__VERIFIER_nondet_i32()

0 → 100644

+26 −0

Original line number	Diff line number	Diff line
		define dso_local i32 @flip(i32 %x) #0 {
		in:
		%res = sub i32 0, %x
		ret i32 %res
		}

		define dso_local i32 @main() #0 {
		in:
		%x = call i32 @__VERIFIER_nondet_i32()
		%cond = icmp slt i32 %x, 0
		br i1 %cond, label %neg, label %join

		neg:
		%p = call i32 @flip(i32 %x)
		br label %join

		join:
		%r = phi i32 [ %p, %neg ], [ %x, %in ]
		%cmp = icmp sge i32 %r, 0
		call void @assert(i1 noundef %cmp)
		ret i32 0
		}

		declare void @assert(i1 noundef) #1

		declare i32 @__VERIFIER_nondet_i32()

0 → 100644

+22 −0

Original line number	Diff line number	Diff line
		define i32 @flip(i32 %x) {
		entry:
		%res = sub i32 0, %x
		ret i32 %res
		}

		define i32 @main() {
		in:
		alloca
		%cond = icmp slt i32 %x, 0
		br i1 %cond, label %neg, label %join

		neg:
		%p = call i32 @flip(i32 %x)
		br label %join

		join:
		%r = phi i32 [ %p, %neg ], [ %x, %in ]
		%cmp = icmp sge i32 %r, 0
		call void @assert(i1 noundef %cmp)
		ret i32 0
		}
		No newline at end of file