search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

ShadowMem is creating a badref #104

Closed caballa closed 4 years ago

caballa commented 4 years ago

Cmd: seadsa --sea-dsa-shadow-mem --log=shadow_verbose ../issue104.ll 

.split:                                           ; preds = %22
  %23 = load i32, i32* <badref>
  call void @shadow.mem.out(i32 19, i32 %23, i32 0, i8* null), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.in(i32 11, i32 %sm6, i32 1, i8* bitcast (i32* @y to i8*)), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.out(i32 11, i32 %shadow.mem.11.0, i32 1, i8* bitcast (i32* @y to i8*)), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.in(i32 15, i32 %sm7, i32 2, i8* bitcast (i32* @x to i8*)), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.out(i32 15, i32 %shadow.mem.15.0, i32 2, i8* bitcast (i32* @x to i8*)), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.out(i32 8, i32 %sm, i32 3, i8* null), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.out(i32 9, i32 %sm1, i32 4, i8* null), !shadow.mem !5, !shadow.mem.use !5
  call void @shadow.mem.out(i32 10, i32 %sm2, i32 5, i8* null), !shadow.mem !5, !shadow.mem.use !5
  ret i32 %.0

issue104.zip

caballa commented 4 years ago

Sorry I created this problem with my commit a393e0e. This should be fixed in commit c3b88ab.