jkbbwr
04/17/2018, 1:37 AMolonho
04/17/2018, 8:46 AMjkbbwr
04/17/2018, 10:54 AM@Kotlin_Int_inc
were not defined in the bitcode, so the verifier couldn't run against them. The seahorn guy worked around it by manually defining them
;;declare i32 @Kotlin_Int_inc(i32)
define i32 @Kotlin_Int_inc(i32) {
entry:
%y = add i32 %0, 1
ret i32 %y
}
olonho
04/17/2018, 11:03 AMjkbbwr
04/17/2018, 11:05 AMolonho
04/17/2018, 11:23 AMjkbbwr
04/17/2018, 11:37 AM