-
Notifications
You must be signed in to change notification settings - Fork 128
Open
Labels
memoryMemory ModelMemory Model
Description
This code seems to not roundtrip to itself:
void use(char&);
void loop() {
char storage[16] = {};
for(char& c : storage) use(c);
}
----------------------------------------
define void @_Z4loopv() {
%entry:
%storage = alloca i64 16, align 16, dead
%0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
start_lifetime * %0
memset * %0 align 16, i8 0, i64 16
%add.ptr = gep inbounds * %storage, 16 x i64 0, 1 x i64 16
br label %for.body
%for.body:
%__begin1.09 = phi * [ %0, %entry ], [ %incdec.ptr, %for.body ]
call void @_Z3useRc(nonnull dereferenceable(1) * %__begin1.09)
%incdec.ptr = gep inbounds * %__begin1.09, 1 x i64 1
%cmp = icmp eq * %incdec.ptr, %add.ptr
br i1 %cmp, label %for.cond.cleanup, label %for.body
%for.cond.cleanup:
free * %0 unconstrained
ret void
}
=>
define void @_Z4loopv() {
%entry:
%storage = alloca i64 16, align 16, dead
%0 = gep inbounds * %storage, 16 x i64 0, 1 x i64 0
start_lifetime * %0
memset * %0 align 16, i8 0, i64 16
%add.ptr = gep inbounds * %storage, 16 x i64 0, 1 x i64 16
br label %for.body
%for.body:
%__begin1.09 = phi * [ %0, %entry ], [ %incdec.ptr, %for.body ]
call void @_Z3useRc(nonnull dereferenceable(1) * %__begin1.09)
%incdec.ptr = gep inbounds * %__begin1.09, 1 x i64 1
%cmp = icmp eq * %incdec.ptr, %add.ptr
br i1 %cmp, label %for.cond.cleanup, label %for.body
%for.cond.cleanup:
free * %0 unconstrained
ret void
}
ERROR: Precondition is always false
Summary:
0 correct transformations
0 incorrect transformations
1 Alive2 errors
I wanted to play around and see what alive2 things about different memsets,
in particular dropping overflowing memset (should fail, but again fails with
ERROR: Precondition is always false
), clamping overflowing memset (should pass,
but again fails with ERROR: Precondition is always false
), etc.
Metadata
Metadata
Assignees
Labels
memoryMemory ModelMemory Model