Created
December 4, 2014 21:30
-
-
Save spacekpe/bbc1be42809921b44510 to your computer and use it in GitHub Desktop.
KLEE demonstration program
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <assert.h> | |
#include <klee/klee.h> | |
int f1(int a, int b) { | |
return a + b; | |
} | |
#define VARIANT 1 | |
int f2(int a, int b) { | |
for (int i = 0; i < sizeof(b) * 8; i++) | |
#if VARIANT == 1 | |
a += (((b >> i) & 1) << i); | |
#else | |
a += (b & (1 << i)); | |
#endif | |
return a; | |
} | |
int main(int argc, char **argv) { | |
int a, b; | |
klee_make_symbolic(&a, sizeof(a), "a"); | |
klee_make_symbolic(&b, sizeof(b), "b"); | |
klee_assert(f1(a, b) == f2(a, b)); | |
return 0; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <assert.h> | |
int f1(int a, int b) { | |
return a + b; | |
} | |
#define VARIANT 1 | |
int f2(int a, int b) { | |
for (int i = 0; i < sizeof(b) * 8; i++) | |
#if VARIANT == 1 | |
a += (((b >> i) & 1) << i); | |
#else | |
a += (b & (1 << i)); | |
#endif | |
return a; | |
} | |
int main(int argc, char **argv) { | |
int a = 124; | |
int b = -2147442176; | |
assert(f1(a, b) == f2(a, b)); | |
return 0; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; ModuleID = 'add-sym.bc' | |
target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" | |
target triple = "x86_64-redhat-linux-gnu" | |
@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1 | |
@.str1 = private unnamed_addr constant [2 x i8] c"b\00", align 1 | |
@.str2 = private unnamed_addr constant [21 x i8] c"f1(a, b) == f2(a, b)\00", align 1 | |
@.str3 = private unnamed_addr constant [10 x i8] c"add-sym.c\00", align 1 | |
@__PRETTY_FUNCTION__.main = private unnamed_addr constant [23 x i8] c"int main(int, char **)\00", align 1 | |
@.str4 = private unnamed_addr constant [67 x i8] c"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_div_zero_check.c\00", align 1 | |
@.str15 = private unnamed_addr constant [15 x i8] c"divide by zero\00", align 1 | |
@.str26 = private unnamed_addr constant [8 x i8] c"div.err\00", align 1 | |
@.str37 = private unnamed_addr constant [8 x i8] c"IGNORED\00", align 1 | |
@.str14 = private unnamed_addr constant [16 x i8] c"overshift error\00", align 1 | |
@.str25 = private unnamed_addr constant [14 x i8] c"overshift.err\00", align 1 | |
@.str6 = private unnamed_addr constant [58 x i8] c"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c\00", align 1 | |
@.str17 = private unnamed_addr constant [14 x i8] c"invalid range\00", align 1 | |
@.str28 = private unnamed_addr constant [5 x i8] c"user\00", align 1 | |
; Function Attrs: nounwind uwtable | |
define i32 @f1(i32 %a, i32 %b) #0 { | |
%1 = alloca i32, align 4 | |
%2 = alloca i32, align 4 | |
store i32 %a, i32* %1, align 4 | |
store i32 %b, i32* %2, align 4 | |
%3 = load i32* %1, align 4 | |
%4 = load i32* %2, align 4 | |
%5 = add nsw i32 %3, %4 | |
ret i32 %5 | |
} | |
; Function Attrs: nounwind uwtable | |
define i32 @f2(i32 %a, i32 %b) #0 { | |
%1 = alloca i32, align 4 | |
%2 = alloca i32, align 4 | |
%i = alloca i32, align 4 | |
store i32 %a, i32* %1, align 4 | |
store i32 %b, i32* %2, align 4 | |
store i32 0, i32* %i, align 4 | |
br label %3 | |
; <label>:3 ; preds = %7, %0 | |
%4 = load i32* %i, align 4 | |
%5 = sext i32 %4 to i64 | |
%6 = icmp ult i64 %5, 32 | |
br i1 %6, label %7, label %18 | |
; <label>:7 ; preds = %3 | |
%8 = load i32* %2, align 4 | |
%9 = load i32* %i, align 4 | |
%int_cast_to_i64 = zext i32 %9 to i64 | |
call void @klee_overshift_check(i64 32, i64 %int_cast_to_i64) | |
%10 = ashr i32 %8, %9 | |
%11 = and i32 %10, 1 | |
%12 = load i32* %i, align 4 | |
%int_cast_to_i641 = zext i32 %12 to i64 | |
call void @klee_overshift_check(i64 32, i64 %int_cast_to_i641) | |
%13 = shl i32 %11, %12 | |
%14 = load i32* %1, align 4 | |
%15 = add nsw i32 %14, %13 | |
store i32 %15, i32* %1, align 4 | |
%16 = load i32* %i, align 4 | |
%17 = add nsw i32 %16, 1 | |
store i32 %17, i32* %i, align 4 | |
br label %3 | |
; <label>:18 ; preds = %3 | |
%19 = load i32* %1, align 4 | |
ret i32 %19 | |
} | |
; Function Attrs: nounwind uwtable | |
define i32 @main(i32 %argc, i8** %argv) #0 { | |
%1 = alloca i32, align 4 | |
%2 = alloca i32, align 4 | |
%3 = alloca i8**, align 8 | |
%a = alloca i32, align 4 | |
%b = alloca i32, align 4 | |
store i32 0, i32* %1 | |
store i32 %argc, i32* %2, align 4 | |
store i8** %argv, i8*** %3, align 8 | |
%4 = bitcast i32* %a to i8* | |
call void @klee_make_symbolic(i8* %4, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0)) | |
%5 = bitcast i32* %b to i8* | |
call void @klee_make_symbolic(i8* %5, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str1, i32 0, i32 0)) | |
%6 = load i32* %a, align 4 | |
%7 = load i32* %b, align 4 | |
%8 = call i32 @f1(i32 %6, i32 %7) | |
%9 = load i32* %a, align 4 | |
%10 = load i32* %b, align 4 | |
%11 = call i32 @f2(i32 %9, i32 %10) | |
%12 = icmp eq i32 %8, %11 | |
br i1 %12, label %14, label %13 | |
; <label>:13 ; preds = %0 | |
call void @__assert_fail(i8* getelementptr inbounds ([21 x i8]* @.str2, i32 0, i32 0), i8* getelementptr inbounds ([10 x i8]* @.str3, i32 0, i32 0), i32 25, i8* getelementptr inbounds ([23 x i8]* @__PRETTY_FUNCTION__.main, i32 0, i32 0)) #7 | |
unreachable | |
; <label>:14 ; preds = %0 | |
ret i32 0 | |
} | |
declare void @klee_make_symbolic(i8*, i64, i8*) #1 | |
; Function Attrs: noreturn nounwind | |
declare void @__assert_fail(i8*, i8*, i32, i8*) #2 | |
; Function Attrs: uwtable | |
define void @klee_div_zero_check(i64 %z) #3 { | |
%1 = icmp eq i64 %z, 0, !dbg !113 | |
br i1 %1, label %2, label %3, !dbg !113 | |
; <label>:2 ; preds = %0 | |
tail call void @klee_report_error(i8* getelementptr inbounds ([67 x i8]* @.str4, i64 0, i64 0), i32 14, i8* getelementptr inbounds ([15 x i8]* @.str15, i64 0, i64 0), i8* getelementptr inbounds ([8 x i8]* @.str26, i64 0, i64 0)) #8, !dbg !115 | |
unreachable, !dbg !115 | |
; <label>:3 ; preds = %0 | |
ret void, !dbg !116 | |
} | |
; Function Attrs: noreturn | |
declare void @klee_report_error(i8*, i32, i8*, i8*) #4 | |
; Function Attrs: nounwind readnone | |
declare void @llvm.dbg.value(metadata, i64, metadata) #5 | |
; Function Attrs: uwtable | |
define i32 @klee_int(i8* %name) #3 { | |
%x = alloca i32, align 4 | |
%1 = bitcast i32* %x to i8*, !dbg !117 | |
call void @klee_make_symbolic(i8* %1, i64 4, i8* %name) #9, !dbg !117 | |
%2 = load i32* %x, align 4, !dbg !118, !tbaa !119 | |
ret i32 %2, !dbg !118 | |
} | |
; Function Attrs: nounwind readnone | |
declare void @llvm.dbg.declare(metadata, metadata) #5 | |
; Function Attrs: uwtable | |
define void @klee_overshift_check(i64 %bitWidth, i64 %shift) #3 { | |
%1 = icmp ult i64 %shift, %bitWidth, !dbg !123 | |
br i1 %1, label %3, label %2, !dbg !123 | |
; <label>:2 ; preds = %0 | |
tail call void @klee_report_error(i8* getelementptr inbounds ([8 x i8]* @.str37, i64 0, i64 0), i32 0, i8* getelementptr inbounds ([16 x i8]* @.str14, i64 0, i64 0), i8* getelementptr inbounds ([14 x i8]* @.str25, i64 0, i64 0)) #8, !dbg !125 | |
unreachable, !dbg !125 | |
; <label>:3 ; preds = %0 | |
ret void, !dbg !127 | |
} | |
; Function Attrs: uwtable | |
define i32 @klee_range(i32 %start, i32 %end, i8* %name) #3 { | |
%x = alloca i32, align 4 | |
%1 = icmp slt i32 %start, %end, !dbg !128 | |
br i1 %1, label %3, label %2, !dbg !128 | |
; <label>:2 ; preds = %0 | |
call void @klee_report_error(i8* getelementptr inbounds ([58 x i8]* @.str6, i64 0, i64 0), i32 17, i8* getelementptr inbounds ([14 x i8]* @.str17, i64 0, i64 0), i8* getelementptr inbounds ([5 x i8]* @.str28, i64 0, i64 0)) #8, !dbg !130 | |
unreachable, !dbg !130 | |
; <label>:3 ; preds = %0 | |
%4 = add nsw i32 %start, 1, !dbg !131 | |
%5 = icmp eq i32 %4, %end, !dbg !131 | |
br i1 %5, label %21, label %6, !dbg !131 | |
; <label>:6 ; preds = %3 | |
%7 = bitcast i32* %x to i8*, !dbg !133 | |
call void @klee_make_symbolic(i8* %7, i64 4, i8* %name) #9, !dbg !133 | |
%8 = icmp eq i32 %start, 0, !dbg !135 | |
%9 = load i32* %x, align 4, !dbg !137, !tbaa !119 | |
br i1 %8, label %10, label %13, !dbg !135 | |
; <label>:10 ; preds = %6 | |
%11 = icmp ult i32 %9, %end, !dbg !137 | |
%12 = zext i1 %11 to i64, !dbg !137 | |
call void @klee_assume(i64 %12) #9, !dbg !137 | |
br label %19, !dbg !139 | |
; <label>:13 ; preds = %6 | |
%14 = icmp sge i32 %9, %start, !dbg !140 | |
%15 = zext i1 %14 to i64, !dbg !140 | |
call void @klee_assume(i64 %15) #9, !dbg !140 | |
%16 = load i32* %x, align 4, !dbg !142, !tbaa !119 | |
%17 = icmp slt i32 %16, %end, !dbg !142 | |
%18 = zext i1 %17 to i64, !dbg !142 | |
call void @klee_assume(i64 %18) #9, !dbg !142 | |
br label %19 | |
; <label>:19 ; preds = %13, %10 | |
%20 = load i32* %x, align 4, !dbg !143, !tbaa !119 | |
br label %21, !dbg !143 | |
; <label>:21 ; preds = %19, %3 | |
%.0 = phi i32 [ %20, %19 ], [ %start, %3 ] | |
ret i32 %.0, !dbg !144 | |
} | |
declare void @klee_assume(i64) #6 | |
; Function Attrs: uwtable | |
define weak i8* @memcpy(i8* %destaddr, i8* %srcaddr, i64 %len) #3 { | |
%1 = icmp eq i64 %len, 0, !dbg !145 | |
br i1 %1, label %._crit_edge, label %.lr.ph.preheader, !dbg !145 | |
.lr.ph.preheader: ; preds = %0 | |
%n.vec = and i64 %len, -32 | |
%cmp.zero = icmp eq i64 %n.vec, 0 | |
%2 = add i64 %len, -1 | |
br i1 %cmp.zero, label %middle.block, label %vector.memcheck | |
vector.memcheck: ; preds = %.lr.ph.preheader | |
%scevgep4 = getelementptr i8* %srcaddr, i64 %2 | |
%scevgep = getelementptr i8* %destaddr, i64 %2 | |
%bound1 = icmp uge i8* %scevgep, %srcaddr | |
%bound0 = icmp uge i8* %scevgep4, %destaddr | |
%memcheck.conflict = and i1 %bound0, %bound1 | |
%ptr.ind.end = getelementptr i8* %srcaddr, i64 %n.vec | |
%ptr.ind.end6 = getelementptr i8* %destaddr, i64 %n.vec | |
%rev.ind.end = sub i64 %len, %n.vec | |
br i1 %memcheck.conflict, label %middle.block, label %vector.body | |
vector.body: ; preds = %vector.body, %vector.memcheck | |
%index = phi i64 [ %index.next, %vector.body ], [ 0, %vector.memcheck ] | |
%next.gep = getelementptr i8* %srcaddr, i64 %index | |
%next.gep103 = getelementptr i8* %destaddr, i64 %index | |
%3 = bitcast i8* %next.gep to <16 x i8>*, !dbg !146 | |
%wide.load = load <16 x i8>* %3, align 1, !dbg !146 | |
%next.gep.sum279 = or i64 %index, 16, !dbg !146 | |
%4 = getelementptr i8* %srcaddr, i64 %next.gep.sum279, !dbg !146 | |
%5 = bitcast i8* %4 to <16 x i8>*, !dbg !146 | |
%wide.load200 = load <16 x i8>* %5, align 1, !dbg !146 | |
%6 = bitcast i8* %next.gep103 to <16 x i8>*, !dbg !146 | |
store <16 x i8> %wide.load, <16 x i8>* %6, align 1, !dbg !146 | |
%7 = getelementptr i8* %destaddr, i64 %next.gep.sum279, !dbg !146 | |
%8 = bitcast i8* %7 to <16 x i8>*, !dbg !146 | |
store <16 x i8> %wide.load200, <16 x i8>* %8, align 1, !dbg !146 | |
%index.next = add i64 %index, 32 | |
%9 = icmp eq i64 %index.next, %n.vec | |
br i1 %9, label %middle.block, label %vector.body, !llvm.loop !147 | |
middle.block: ; preds = %vector.body, %vector.memcheck, %.lr.ph.preheader | |
%resume.val = phi i8* [ %srcaddr, %.lr.ph.preheader ], [ %srcaddr, %vector.memcheck ], [ %ptr.ind.end, %vector.body ] | |
%resume.val5 = phi i8* [ %destaddr, %.lr.ph.preheader ], [ %destaddr, %vector.memcheck ], [ %ptr.ind.end6, %vector.body ] | |
%resume.val7 = phi i64 [ %len, %.lr.ph.preheader ], [ %len, %vector.memcheck ], [ %rev.ind.end, %vector.body ] | |
%new.indc.resume.val = phi i64 [ 0, %.lr.ph.preheader ], [ 0, %vector.memcheck ], [ %n.vec, %vector.body ] | |
%cmp.n = icmp eq i64 %new.indc.resume.val, %len | |
br i1 %cmp.n, label %._crit_edge, label %.lr.ph | |
.lr.ph: ; preds = %.lr.ph, %middle.block | |
%src.03 = phi i8* [ %11, %.lr.ph ], [ %resume.val, %middle.block ] | |
%dest.02 = phi i8* [ %13, %.lr.ph ], [ %resume.val5, %middle.block ] | |
%.01 = phi i64 [ %10, %.lr.ph ], [ %resume.val7, %middle.block ] | |
%10 = add i64 %.01, -1, !dbg !145 | |
%11 = getelementptr inbounds i8* %src.03, i64 1, !dbg !146 | |
%12 = load i8* %src.03, align 1, !dbg !146, !tbaa !150 | |
%13 = getelementptr inbounds i8* %dest.02, i64 1, !dbg !146 | |
store i8 %12, i8* %dest.02, align 1, !dbg !146, !tbaa !150 | |
%14 = icmp eq i64 %10, 0, !dbg !145 | |
br i1 %14, label %._crit_edge, label %.lr.ph, !dbg !145, !llvm.loop !151 | |
._crit_edge: ; preds = %.lr.ph, %middle.block, %0 | |
ret i8* %destaddr, !dbg !152 | |
} | |
; Function Attrs: uwtable | |
define weak i8* @memmove(i8* %dst, i8* %src, i64 %count) #3 { | |
%1 = icmp eq i8* %src, %dst, !dbg !153 | |
br i1 %1, label %.loopexit, label %2, !dbg !153 | |
; <label>:2 ; preds = %0 | |
%3 = icmp ugt i8* %src, %dst, !dbg !155 | |
br i1 %3, label %.preheader, label %18, !dbg !155 | |
.preheader: ; preds = %2 | |
%4 = icmp eq i64 %count, 0, !dbg !157 | |
br i1 %4, label %.loopexit, label %.lr.ph.preheader, !dbg !157 | |
.lr.ph.preheader: ; preds = %.preheader | |
%n.vec = and i64 %count, -32 | |
%cmp.zero = icmp eq i64 %n.vec, 0 | |
%5 = add i64 %count, -1 | |
br i1 %cmp.zero, label %middle.block, label %vector.memcheck | |
vector.memcheck: ; preds = %.lr.ph.preheader | |
%scevgep11 = getelementptr i8* %src, i64 %5 | |
%scevgep = getelementptr i8* %dst, i64 %5 | |
%bound1 = icmp uge i8* %scevgep, %src | |
%bound0 = icmp uge i8* %scevgep11, %dst | |
%memcheck.conflict = and i1 %bound0, %bound1 | |
%ptr.ind.end = getelementptr i8* %src, i64 %n.vec | |
%ptr.ind.end13 = getelementptr i8* %dst, i64 %n.vec | |
%rev.ind.end = sub i64 %count, %n.vec | |
br i1 %memcheck.conflict, label %middle.block, label %vector.body | |
vector.body: ; preds = %vector.body, %vector.memcheck | |
%index = phi i64 [ %index.next, %vector.body ], [ 0, %vector.memcheck ] | |
%next.gep = getelementptr i8* %src, i64 %index | |
%next.gep110 = getelementptr i8* %dst, i64 %index | |
%6 = bitcast i8* %next.gep to <16 x i8>*, !dbg !157 | |
%wide.load = load <16 x i8>* %6, align 1, !dbg !157 | |
%next.gep.sum586 = or i64 %index, 16, !dbg !157 | |
%7 = getelementptr i8* %src, i64 %next.gep.sum586, !dbg !157 | |
%8 = bitcast i8* %7 to <16 x i8>*, !dbg !157 | |
%wide.load207 = load <16 x i8>* %8, align 1, !dbg !157 | |
%9 = bitcast i8* %next.gep110 to <16 x i8>*, !dbg !157 | |
store <16 x i8> %wide.load, <16 x i8>* %9, align 1, !dbg !157 | |
%10 = getelementptr i8* %dst, i64 %next.gep.sum586, !dbg !157 | |
%11 = bitcast i8* %10 to <16 x i8>*, !dbg !157 | |
store <16 x i8> %wide.load207, <16 x i8>* %11, align 1, !dbg !157 | |
%index.next = add i64 %index, 32 | |
%12 = icmp eq i64 %index.next, %n.vec | |
br i1 %12, label %middle.block, label %vector.body, !llvm.loop !159 | |
middle.block: ; preds = %vector.body, %vector.memcheck, %.lr.ph.preheader | |
%resume.val = phi i8* [ %src, %.lr.ph.preheader ], [ %src, %vector.memcheck ], [ %ptr.ind.end, %vector.body ] | |
%resume.val12 = phi i8* [ %dst, %.lr.ph.preheader ], [ %dst, %vector.memcheck ], [ %ptr.ind.end13, %vector.body ] | |
%resume.val14 = phi i64 [ %count, %.lr.ph.preheader ], [ %count, %vector.memcheck ], [ %rev.ind.end, %vector.body ] | |
%new.indc.resume.val = phi i64 [ 0, %.lr.ph.preheader ], [ 0, %vector.memcheck ], [ %n.vec, %vector.body ] | |
%cmp.n = icmp eq i64 %new.indc.resume.val, %count | |
br i1 %cmp.n, label %.loopexit, label %.lr.ph | |
.lr.ph: ; preds = %.lr.ph, %middle.block | |
%b.04 = phi i8* [ %14, %.lr.ph ], [ %resume.val, %middle.block ] | |
%a.03 = phi i8* [ %16, %.lr.ph ], [ %resume.val12, %middle.block ] | |
%.02 = phi i64 [ %13, %.lr.ph ], [ %resume.val14, %middle.block ] | |
%13 = add i64 %.02, -1, !dbg !157 | |
%14 = getelementptr inbounds i8* %b.04, i64 1, !dbg !157 | |
%15 = load i8* %b.04, align 1, !dbg !157, !tbaa !150 | |
%16 = getelementptr inbounds i8* %a.03, i64 1, !dbg !157 | |
store i8 %15, i8* %a.03, align 1, !dbg !157, !tbaa !150 | |
%17 = icmp eq i64 %13, 0, !dbg !157 | |
br i1 %17, label %.loopexit, label %.lr.ph, !dbg !157, !llvm.loop !160 | |
; <label>:18 ; preds = %2 | |
%19 = add i64 %count, -1, !dbg !161 | |
%20 = icmp eq i64 %count, 0, !dbg !163 | |
br i1 %20, label %.loopexit, label %.lr.ph9, !dbg !163 | |
.lr.ph9: ; preds = %18 | |
%21 = getelementptr inbounds i8* %src, i64 %19, !dbg !164 | |
%22 = getelementptr inbounds i8* %dst, i64 %19, !dbg !161 | |
%n.vec215 = and i64 %count, -32 | |
%cmp.zero217 = icmp eq i64 %n.vec215, 0 | |
br i1 %cmp.zero217, label %middle.block210, label %vector.memcheck224 | |
vector.memcheck224: ; preds = %.lr.ph9 | |
%bound1221 = icmp ule i8* %21, %dst | |
%bound0220 = icmp ule i8* %22, %src | |
%memcheck.conflict223 = and i1 %bound0220, %bound1221 | |
%.sum = sub i64 %19, %n.vec215 | |
%rev.ptr.ind.end = getelementptr i8* %src, i64 %.sum | |
%rev.ptr.ind.end229 = getelementptr i8* %dst, i64 %.sum | |
%rev.ind.end231 = sub i64 %count, %n.vec215 | |
br i1 %memcheck.conflict223, label %middle.block210, label %vector.body209 | |
vector.body209: ; preds = %vector.body209, %vector.memcheck224 | |
%index212 = phi i64 [ %index.next234, %vector.body209 ], [ 0, %vector.memcheck224 ] | |
%.sum440 = sub i64 %19, %index212 | |
%next.gep236.sum = add i64 %.sum440, -15, !dbg !163 | |
%23 = getelementptr i8* %src, i64 %next.gep236.sum, !dbg !163 | |
%24 = bitcast i8* %23 to <16 x i8>*, !dbg !163 | |
%wide.load434 = load <16 x i8>* %24, align 1, !dbg !163 | |
%reverse = shufflevector <16 x i8> %wide.load434, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !163 | |
%.sum505 = add i64 %.sum440, -31, !dbg !163 | |
%25 = getelementptr i8* %src, i64 %.sum505, !dbg !163 | |
%26 = bitcast i8* %25 to <16 x i8>*, !dbg !163 | |
%wide.load435 = load <16 x i8>* %26, align 1, !dbg !163 | |
%reverse436 = shufflevector <16 x i8> %wide.load435, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !163 | |
%reverse437 = shufflevector <16 x i8> %reverse, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !163 | |
%27 = getelementptr i8* %dst, i64 %next.gep236.sum, !dbg !163 | |
%28 = bitcast i8* %27 to <16 x i8>*, !dbg !163 | |
store <16 x i8> %reverse437, <16 x i8>* %28, align 1, !dbg !163 | |
%reverse438 = shufflevector <16 x i8> %reverse436, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !163 | |
%29 = getelementptr i8* %dst, i64 %.sum505, !dbg !163 | |
%30 = bitcast i8* %29 to <16 x i8>*, !dbg !163 | |
store <16 x i8> %reverse438, <16 x i8>* %30, align 1, !dbg !163 | |
%index.next234 = add i64 %index212, 32 | |
%31 = icmp eq i64 %index.next234, %n.vec215 | |
br i1 %31, label %middle.block210, label %vector.body209, !llvm.loop !165 | |
middle.block210: ; preds = %vector.body209, %vector.memcheck224, %.lr.ph9 | |
%resume.val225 = phi i8* [ %21, %.lr.ph9 ], [ %21, %vector.memcheck224 ], [ %rev.ptr.ind.end, %vector.body209 ] | |
%resume.val227 = phi i8* [ %22, %.lr.ph9 ], [ %22, %vector.memcheck224 ], [ %rev.ptr.ind.end229, %vector.body209 ] | |
%resume.val230 = phi i64 [ %count, %.lr.ph9 ], [ %count, %vector.memcheck224 ], [ %rev.ind.end231, %vector.body209 ] | |
%new.indc.resume.val232 = phi i64 [ 0, %.lr.ph9 ], [ 0, %vector.memcheck224 ], [ %n.vec215, %vector.body209 ] | |
%cmp.n233 = icmp eq i64 %new.indc.resume.val232, %count | |
br i1 %cmp.n233, label %.loopexit, label %scalar.ph211 | |
scalar.ph211: ; preds = %scalar.ph211, %middle.block210 | |
%b.18 = phi i8* [ %33, %scalar.ph211 ], [ %resume.val225, %middle.block210 ] | |
%a.17 = phi i8* [ %35, %scalar.ph211 ], [ %resume.val227, %middle.block210 ] | |
%.16 = phi i64 [ %32, %scalar.ph211 ], [ %resume.val230, %middle.block210 ] | |
%32 = add i64 %.16, -1, !dbg !163 | |
%33 = getelementptr inbounds i8* %b.18, i64 -1, !dbg !163 | |
%34 = load i8* %b.18, align 1, !dbg !163, !tbaa !150 | |
%35 = getelementptr inbounds i8* %a.17, i64 -1, !dbg !163 | |
store i8 %34, i8* %a.17, align 1, !dbg !163, !tbaa !150 | |
%36 = icmp eq i64 %32, 0, !dbg !163 | |
br i1 %36, label %.loopexit, label %scalar.ph211, !dbg !163, !llvm.loop !166 | |
.loopexit: ; preds = %scalar.ph211, %middle.block210, %18, %.lr.ph, %middle.block, %.preheader, %0 | |
ret i8* %dst, !dbg !167 | |
} | |
; Function Attrs: uwtable | |
define weak i8* @mempcpy(i8* %destaddr, i8* %srcaddr, i64 %len) #3 { | |
%1 = icmp eq i64 %len, 0, !dbg !168 | |
br i1 %1, label %15, label %.lr.ph.preheader, !dbg !168 | |
.lr.ph.preheader: ; preds = %0 | |
%n.vec = and i64 %len, -32 | |
%cmp.zero = icmp eq i64 %n.vec, 0 | |
%2 = add i64 %len, -1 | |
br i1 %cmp.zero, label %middle.block, label %vector.memcheck | |
vector.memcheck: ; preds = %.lr.ph.preheader | |
%scevgep5 = getelementptr i8* %srcaddr, i64 %2 | |
%scevgep4 = getelementptr i8* %destaddr, i64 %2 | |
%bound1 = icmp uge i8* %scevgep4, %srcaddr | |
%bound0 = icmp uge i8* %scevgep5, %destaddr | |
%memcheck.conflict = and i1 %bound0, %bound1 | |
%ptr.ind.end = getelementptr i8* %srcaddr, i64 %n.vec | |
%ptr.ind.end7 = getelementptr i8* %destaddr, i64 %n.vec | |
%rev.ind.end = sub i64 %len, %n.vec | |
br i1 %memcheck.conflict, label %middle.block, label %vector.body | |
vector.body: ; preds = %vector.body, %vector.memcheck | |
%index = phi i64 [ %index.next, %vector.body ], [ 0, %vector.memcheck ] | |
%next.gep = getelementptr i8* %srcaddr, i64 %index | |
%next.gep104 = getelementptr i8* %destaddr, i64 %index | |
%3 = bitcast i8* %next.gep to <16 x i8>*, !dbg !169 | |
%wide.load = load <16 x i8>* %3, align 1, !dbg !169 | |
%next.gep.sum280 = or i64 %index, 16, !dbg !169 | |
%4 = getelementptr i8* %srcaddr, i64 %next.gep.sum280, !dbg !169 | |
%5 = bitcast i8* %4 to <16 x i8>*, !dbg !169 | |
%wide.load201 = load <16 x i8>* %5, align 1, !dbg !169 | |
%6 = bitcast i8* %next.gep104 to <16 x i8>*, !dbg !169 | |
store <16 x i8> %wide.load, <16 x i8>* %6, align 1, !dbg !169 | |
%7 = getelementptr i8* %destaddr, i64 %next.gep.sum280, !dbg !169 | |
%8 = bitcast i8* %7 to <16 x i8>*, !dbg !169 | |
store <16 x i8> %wide.load201, <16 x i8>* %8, align 1, !dbg !169 | |
%index.next = add i64 %index, 32 | |
%9 = icmp eq i64 %index.next, %n.vec | |
br i1 %9, label %middle.block, label %vector.body, !llvm.loop !170 | |
middle.block: ; preds = %vector.body, %vector.memcheck, %.lr.ph.preheader | |
%resume.val = phi i8* [ %srcaddr, %.lr.ph.preheader ], [ %srcaddr, %vector.memcheck ], [ %ptr.ind.end, %vector.body ] | |
%resume.val6 = phi i8* [ %destaddr, %.lr.ph.preheader ], [ %destaddr, %vector.memcheck ], [ %ptr.ind.end7, %vector.body ] | |
%resume.val8 = phi i64 [ %len, %.lr.ph.preheader ], [ %len, %vector.memcheck ], [ %rev.ind.end, %vector.body ] | |
%new.indc.resume.val = phi i64 [ 0, %.lr.ph.preheader ], [ 0, %vector.memcheck ], [ %n.vec, %vector.body ] | |
%cmp.n = icmp eq i64 %new.indc.resume.val, %len | |
br i1 %cmp.n, label %._crit_edge, label %.lr.ph | |
.lr.ph: ; preds = %.lr.ph, %middle.block | |
%src.03 = phi i8* [ %11, %.lr.ph ], [ %resume.val, %middle.block ] | |
%dest.02 = phi i8* [ %13, %.lr.ph ], [ %resume.val6, %middle.block ] | |
%.01 = phi i64 [ %10, %.lr.ph ], [ %resume.val8, %middle.block ] | |
%10 = add i64 %.01, -1, !dbg !168 | |
%11 = getelementptr inbounds i8* %src.03, i64 1, !dbg !169 | |
%12 = load i8* %src.03, align 1, !dbg !169, !tbaa !150 | |
%13 = getelementptr inbounds i8* %dest.02, i64 1, !dbg !169 | |
store i8 %12, i8* %dest.02, align 1, !dbg !169, !tbaa !150 | |
%14 = icmp eq i64 %10, 0, !dbg !168 | |
br i1 %14, label %._crit_edge, label %.lr.ph, !dbg !168, !llvm.loop !171 | |
._crit_edge: ; preds = %.lr.ph, %middle.block | |
%scevgep = getelementptr i8* %destaddr, i64 %len | |
br label %15, !dbg !168 | |
; <label>:15 ; preds = %._crit_edge, %0 | |
%dest.0.lcssa = phi i8* [ %scevgep, %._crit_edge ], [ %destaddr, %0 ] | |
ret i8* %dest.0.lcssa, !dbg !172 | |
} | |
; Function Attrs: uwtable | |
define weak i8* @memset(i8* %dst, i32 %s, i64 %count) #3 { | |
%1 = icmp eq i64 %count, 0, !dbg !173 | |
br i1 %1, label %._crit_edge, label %.lr.ph, !dbg !173 | |
.lr.ph: ; preds = %0 | |
%2 = trunc i32 %s to i8, !dbg !174 | |
br label %3, !dbg !173 | |
; <label>:3 ; preds = %3, %.lr.ph | |
%a.02 = phi i8* [ %dst, %.lr.ph ], [ %5, %3 ] | |
%.01 = phi i64 [ %count, %.lr.ph ], [ %4, %3 ] | |
%4 = add i64 %.01, -1, !dbg !173 | |
%5 = getelementptr inbounds i8* %a.02, i64 1, !dbg !174 | |
store volatile i8 %2, i8* %a.02, align 1, !dbg !174, !tbaa !150 | |
%6 = icmp eq i64 %4, 0, !dbg !173 | |
br i1 %6, label %._crit_edge, label %3, !dbg !173 | |
._crit_edge: ; preds = %3, %0 | |
ret i8* %dst, !dbg !175 | |
} | |
attributes #0 = { nounwind uwtable "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float | |
attributes #1 = { "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #2 = { noreturn nounwind "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-floa | |
attributes #3 = { uwtable "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #4 = { noreturn "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #5 = { nounwind readnone } | |
attributes #6 = { "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #7 = { noreturn nounwind } | |
attributes #8 = { nobuiltin noreturn } | |
attributes #9 = { nobuiltin } | |
!llvm.ident = !{!0, !0, !0, !0, !0, !0, !0, !0, !0} | |
!llvm.dbg.cu = !{!1, !12, !26, !37, !49, !68, !82, !96} | |
!llvm.module.flags = !{!111, !112} | |
!0 = metadata !{metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)"} | |
!1 = metadata !{i32 786449, metadata !2, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !4, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home/ps | |
!2 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_div_zero_check.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!3 = metadata !{i32 0} | |
!4 = metadata !{metadata !5} | |
!5 = metadata !{i32 786478, metadata !2, metadata !6, metadata !"klee_div_zero_check", metadata !"klee_div_zero_check", metadata !"", i32 12, metadata !7, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, void (i64)* @klee_div_zero_check, null, nu | |
!6 = metadata !{i32 786473, metadata !2} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_div_zero_check.c] | |
!7 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !8, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!8 = metadata !{null, metadata !9} | |
!9 = metadata !{i32 786468, null, null, metadata !"long long int", i32 0, i64 64, i64 64, i64 0, i32 0, i32 5} ; [ DW_TAG_base_type ] [long long int] [line 0, size 64, align 64, offset 0, enc DW_ATE_signed] | |
!10 = metadata !{metadata !11} | |
!11 = metadata !{i32 786689, metadata !5, metadata !"z", metadata !6, i32 16777228, metadata !9, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [z] [line 12] | |
!12 = metadata !{i32 786449, metadata !13, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !14, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!13 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_int.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!14 = metadata !{metadata !15} | |
!15 = metadata !{i32 786478, metadata !13, metadata !16, metadata !"klee_int", metadata !"klee_int", metadata !"", i32 13, metadata !17, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i32 (i8*)* @klee_int, null, null, metadata !23, i32 13} ; [ | |
!16 = metadata !{i32 786473, metadata !13} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_int.c] | |
!17 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !18, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!18 = metadata !{metadata !19, metadata !20} | |
!19 = metadata !{i32 786468, null, null, metadata !"int", i32 0, i64 32, i64 32, i64 0, i32 0, i32 5} ; [ DW_TAG_base_type ] [int] [line 0, size 32, align 32, offset 0, enc DW_ATE_signed] | |
!20 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !21} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from ] | |
!21 = metadata !{i32 786470, null, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, metadata !22} ; [ DW_TAG_const_type ] [line 0, size 0, align 0, offset 0] [from char] | |
!22 = metadata !{i32 786468, null, null, metadata !"char", i32 0, i64 8, i64 8, i64 0, i32 0, i32 6} ; [ DW_TAG_base_type ] [char] [line 0, size 8, align 8, offset 0, enc DW_ATE_signed_char] | |
!23 = metadata !{metadata !24, metadata !25} | |
!24 = metadata !{i32 786689, metadata !15, metadata !"name", metadata !16, i32 16777229, metadata !20, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [name] [line 13] | |
!25 = metadata !{i32 786688, metadata !15, metadata !"x", metadata !16, i32 14, metadata !19, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [x] [line 14] | |
!26 = metadata !{i32 786449, metadata !27, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !28, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!27 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_overshift_check.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!28 = metadata !{metadata !29} | |
!29 = metadata !{i32 786478, metadata !27, metadata !30, metadata !"klee_overshift_check", metadata !"klee_overshift_check", metadata !"", i32 20, metadata !31, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, void (i64, i64)* @klee_overshift_che | |
!30 = metadata !{i32 786473, metadata !27} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_overshift_check.c] | |
!31 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !32, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!32 = metadata !{null, metadata !33, metadata !33} | |
!33 = metadata !{i32 786468, null, null, metadata !"long long unsigned int", i32 0, i64 64, i64 64, i64 0, i32 0, i32 7} ; [ DW_TAG_base_type ] [long long unsigned int] [line 0, size 64, align 64, offset 0, enc DW_ATE_unsigned] | |
!34 = metadata !{metadata !35, metadata !36} | |
!35 = metadata !{i32 786689, metadata !29, metadata !"bitWidth", metadata !30, i32 16777236, metadata !33, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [bitWidth] [line 20] | |
!36 = metadata !{i32 786689, metadata !29, metadata !"shift", metadata !30, i32 33554452, metadata !33, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [shift] [line 20] | |
!37 = metadata !{i32 786449, metadata !38, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !39, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!38 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!39 = metadata !{metadata !40} | |
!40 = metadata !{i32 786478, metadata !38, metadata !41, metadata !"klee_range", metadata !"klee_range", metadata !"", i32 13, metadata !42, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i32 (i32, i32, i8*)* @klee_range, null, null, metadata ! | |
!41 = metadata !{i32 786473, metadata !38} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!42 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !43, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!43 = metadata !{metadata !19, metadata !19, metadata !19, metadata !20} | |
!44 = metadata !{metadata !45, metadata !46, metadata !47, metadata !48} | |
!45 = metadata !{i32 786689, metadata !40, metadata !"start", metadata !41, i32 16777229, metadata !19, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [start] [line 13] | |
!46 = metadata !{i32 786689, metadata !40, metadata !"end", metadata !41, i32 33554445, metadata !19, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [end] [line 13] | |
!47 = metadata !{i32 786689, metadata !40, metadata !"name", metadata !41, i32 50331661, metadata !20, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [name] [line 13] | |
!48 = metadata !{i32 786688, metadata !40, metadata !"x", metadata !41, i32 14, metadata !19, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [x] [line 14] | |
!49 = metadata !{i32 786449, metadata !50, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !51, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!50 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/memcpy.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!51 = metadata !{metadata !52} | |
!52 = metadata !{i32 786478, metadata !50, metadata !53, metadata !"memcpy", metadata !"memcpy", metadata !"", i32 12, metadata !54, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i8* (i8*, i8*, i64)* @memcpy, null, null, metadata !61, i32 12} | |
!53 = metadata !{i32 786473, metadata !50} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memcpy.c] | |
!54 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !55, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!55 = metadata !{metadata !56, metadata !56, metadata !57, metadata !59} | |
!56 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, null} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from ] | |
!57 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !58} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from ] | |
!58 = metadata !{i32 786470, null, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null} ; [ DW_TAG_const_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!59 = metadata !{i32 786454, metadata !50, null, metadata !"size_t", i32 42, i64 0, i64 0, i64 0, i32 0, metadata !60} ; [ DW_TAG_typedef ] [size_t] [line 42, size 0, align 0, offset 0] [from long unsigned int] | |
!60 = metadata !{i32 786468, null, null, metadata !"long unsigned int", i32 0, i64 64, i64 64, i64 0, i32 0, i32 7} ; [ DW_TAG_base_type ] [long unsigned int] [line 0, size 64, align 64, offset 0, enc DW_ATE_unsigned] | |
!61 = metadata !{metadata !62, metadata !63, metadata !64, metadata !65, metadata !67} | |
!62 = metadata !{i32 786689, metadata !52, metadata !"destaddr", metadata !53, i32 16777228, metadata !56, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [destaddr] [line 12] | |
!63 = metadata !{i32 786689, metadata !52, metadata !"srcaddr", metadata !53, i32 33554444, metadata !57, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [srcaddr] [line 12] | |
!64 = metadata !{i32 786689, metadata !52, metadata !"len", metadata !53, i32 50331660, metadata !59, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [len] [line 12] | |
!65 = metadata !{i32 786688, metadata !52, metadata !"dest", metadata !53, i32 13, metadata !66, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [dest] [line 13] | |
!66 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !22} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from char] | |
!67 = metadata !{i32 786688, metadata !52, metadata !"src", metadata !53, i32 14, metadata !20, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [src] [line 14] | |
!68 = metadata !{i32 786449, metadata !69, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !70, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!69 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!70 = metadata !{metadata !71} | |
!71 = metadata !{i32 786478, metadata !69, metadata !72, metadata !"memmove", metadata !"memmove", metadata !"", i32 12, metadata !73, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i8* (i8*, i8*, i64)* @memmove, null, null, metadata !76, i32 1 | |
!72 = metadata !{i32 786473, metadata !69} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c] | |
!73 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !74, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!74 = metadata !{metadata !56, metadata !56, metadata !57, metadata !75} | |
!75 = metadata !{i32 786454, metadata !69, null, metadata !"size_t", i32 42, i64 0, i64 0, i64 0, i32 0, metadata !60} ; [ DW_TAG_typedef ] [size_t] [line 42, size 0, align 0, offset 0] [from long unsigned int] | |
!76 = metadata !{metadata !77, metadata !78, metadata !79, metadata !80, metadata !81} | |
!77 = metadata !{i32 786689, metadata !71, metadata !"dst", metadata !72, i32 16777228, metadata !56, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [dst] [line 12] | |
!78 = metadata !{i32 786689, metadata !71, metadata !"src", metadata !72, i32 33554444, metadata !57, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [src] [line 12] | |
!79 = metadata !{i32 786689, metadata !71, metadata !"count", metadata !72, i32 50331660, metadata !75, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [count] [line 12] | |
!80 = metadata !{i32 786688, metadata !71, metadata !"a", metadata !72, i32 13, metadata !66, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [a] [line 13] | |
!81 = metadata !{i32 786688, metadata !71, metadata !"b", metadata !72, i32 14, metadata !20, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [b] [line 14] | |
!82 = metadata !{i32 786449, metadata !83, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !84, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!83 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/mempcpy.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!84 = metadata !{metadata !85} | |
!85 = metadata !{i32 786478, metadata !83, metadata !86, metadata !"mempcpy", metadata !"mempcpy", metadata !"", i32 11, metadata !87, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i8* (i8*, i8*, i64)* @mempcpy, null, null, metadata !90, i32 1 | |
!86 = metadata !{i32 786473, metadata !83} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/mempcpy.c] | |
!87 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !88, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!88 = metadata !{metadata !56, metadata !56, metadata !57, metadata !89} | |
!89 = metadata !{i32 786454, metadata !83, null, metadata !"size_t", i32 42, i64 0, i64 0, i64 0, i32 0, metadata !60} ; [ DW_TAG_typedef ] [size_t] [line 42, size 0, align 0, offset 0] [from long unsigned int] | |
!90 = metadata !{metadata !91, metadata !92, metadata !93, metadata !94, metadata !95} | |
!91 = metadata !{i32 786689, metadata !85, metadata !"destaddr", metadata !86, i32 16777227, metadata !56, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [destaddr] [line 11] | |
!92 = metadata !{i32 786689, metadata !85, metadata !"srcaddr", metadata !86, i32 33554443, metadata !57, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [srcaddr] [line 11] | |
!93 = metadata !{i32 786689, metadata !85, metadata !"len", metadata !86, i32 50331659, metadata !89, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [len] [line 11] | |
!94 = metadata !{i32 786688, metadata !85, metadata !"dest", metadata !86, i32 12, metadata !66, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [dest] [line 12] | |
!95 = metadata !{i32 786688, metadata !85, metadata !"src", metadata !86, i32 13, metadata !20, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [src] [line 13] | |
!96 = metadata !{i32 786449, metadata !97, i32 1, metadata !"clang version 3.4.2 (tags/RELEASE_34/dot2-final)", i1 true, metadata !"", i32 0, metadata !3, metadata !3, metadata !98, metadata !3, metadata !3, metadata !""} ; [ DW_TAG_compile_unit ] [/home | |
!97 = metadata !{metadata !"/home/pspacek/pkg/klee/git/runtime/Intrinsic/memset.c", metadata !"/home/pspacek/pkg/klee/git/build/runtime/Intrinsic"} | |
!98 = metadata !{metadata !99} | |
!99 = metadata !{i32 786478, metadata !97, metadata !100, metadata !"memset", metadata !"memset", metadata !"", i32 11, metadata !101, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, i8* (i8*, i32, i64)* @memset, null, null, metadata !104, i32 1 | |
!100 = metadata !{i32 786473, metadata !97} ; [ DW_TAG_file_type ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memset.c] | |
!101 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !102, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] | |
!102 = metadata !{metadata !56, metadata !56, metadata !19, metadata !103} | |
!103 = metadata !{i32 786454, metadata !97, null, metadata !"size_t", i32 42, i64 0, i64 0, i64 0, i32 0, metadata !60} ; [ DW_TAG_typedef ] [size_t] [line 42, size 0, align 0, offset 0] [from long unsigned int] | |
!104 = metadata !{metadata !105, metadata !106, metadata !107, metadata !108} | |
!105 = metadata !{i32 786689, metadata !99, metadata !"dst", metadata !100, i32 16777227, metadata !56, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [dst] [line 11] | |
!106 = metadata !{i32 786689, metadata !99, metadata !"s", metadata !100, i32 33554443, metadata !19, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [s] [line 11] | |
!107 = metadata !{i32 786689, metadata !99, metadata !"count", metadata !100, i32 50331659, metadata !103, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [count] [line 11] | |
!108 = metadata !{i32 786688, metadata !99, metadata !"a", metadata !100, i32 12, metadata !109, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [a] [line 12] | |
!109 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !110} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from ] | |
!110 = metadata !{i32 786485, null, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, metadata !22} ; [ DW_TAG_volatile_type ] [line 0, size 0, align 0, offset 0] [from char] | |
!111 = metadata !{i32 2, metadata !"Dwarf Version", i32 4} | |
!112 = metadata !{i32 1, metadata !"Debug Info Version", i32 1} | |
!113 = metadata !{i32 13, i32 0, metadata !114, null} | |
!114 = metadata !{i32 786443, metadata !2, metadata !5, i32 13, i32 0, i32 0} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_div_zero_check.c] | |
!115 = metadata !{i32 14, i32 0, metadata !114, null} | |
!116 = metadata !{i32 15, i32 0, metadata !5, null} | |
!117 = metadata !{i32 15, i32 0, metadata !15, null} | |
!118 = metadata !{i32 16, i32 0, metadata !15, null} | |
!119 = metadata !{metadata !120, metadata !120, i64 0} | |
!120 = metadata !{metadata !"int", metadata !121, i64 0} | |
!121 = metadata !{metadata !"omnipotent char", metadata !122, i64 0} | |
!122 = metadata !{metadata !"Simple C/C++ TBAA"} | |
!123 = metadata !{i32 21, i32 0, metadata !124, null} | |
!124 = metadata !{i32 786443, metadata !27, metadata !29, i32 21, i32 0, i32 0} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_overshift_check.c] | |
!125 = metadata !{i32 27, i32 0, metadata !126, null} | |
!126 = metadata !{i32 786443, metadata !27, metadata !124, i32 21, i32 0, i32 1} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_overshift_check.c] | |
!127 = metadata !{i32 29, i32 0, metadata !29, null} | |
!128 = metadata !{i32 16, i32 0, metadata !129, null} | |
!129 = metadata !{i32 786443, metadata !38, metadata !40, i32 16, i32 0, i32 0} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!130 = metadata !{i32 17, i32 0, metadata !129, null} | |
!131 = metadata !{i32 19, i32 0, metadata !132, null} | |
!132 = metadata !{i32 786443, metadata !38, metadata !40, i32 19, i32 0, i32 1} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!133 = metadata !{i32 22, i32 0, metadata !134, null} | |
!134 = metadata !{i32 786443, metadata !38, metadata !132, i32 21, i32 0, i32 3} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!135 = metadata !{i32 25, i32 0, metadata !136, null} | |
!136 = metadata !{i32 786443, metadata !38, metadata !134, i32 25, i32 0, i32 4} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!137 = metadata !{i32 26, i32 0, metadata !138, null} | |
!138 = metadata !{i32 786443, metadata !38, metadata !136, i32 25, i32 0, i32 5} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!139 = metadata !{i32 27, i32 0, metadata !138, null} | |
!140 = metadata !{i32 28, i32 0, metadata !141, null} | |
!141 = metadata !{i32 786443, metadata !38, metadata !136, i32 27, i32 0, i32 6} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/klee_range.c] | |
!142 = metadata !{i32 29, i32 0, metadata !141, null} | |
!143 = metadata !{i32 32, i32 0, metadata !134, null} | |
!144 = metadata !{i32 34, i32 0, metadata !40, null} | |
!145 = metadata !{i32 16, i32 0, metadata !52, null} | |
!146 = metadata !{i32 17, i32 0, metadata !52, null} | |
!147 = metadata !{metadata !147, metadata !148, metadata !149} | |
!148 = metadata !{metadata !"llvm.vectorizer.width", i32 1} | |
!149 = metadata !{metadata !"llvm.vectorizer.unroll", i32 1} | |
!150 = metadata !{metadata !121, metadata !121, i64 0} | |
!151 = metadata !{metadata !151, metadata !148, metadata !149} | |
!152 = metadata !{i32 18, i32 0, metadata !52, null} | |
!153 = metadata !{i32 16, i32 0, metadata !154, null} | |
!154 = metadata !{i32 786443, metadata !69, metadata !71, i32 16, i32 0, i32 0} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c] | |
!155 = metadata !{i32 19, i32 0, metadata !156, null} | |
!156 = metadata !{i32 786443, metadata !69, metadata !71, i32 19, i32 0, i32 1} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c] | |
!157 = metadata !{i32 20, i32 0, metadata !158, null} | |
!158 = metadata !{i32 786443, metadata !69, metadata !156, i32 19, i32 0, i32 2} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c] | |
!159 = metadata !{metadata !159, metadata !148, metadata !149} | |
!160 = metadata !{metadata !160, metadata !148, metadata !149} | |
!161 = metadata !{i32 22, i32 0, metadata !162, null} | |
!162 = metadata !{i32 786443, metadata !69, metadata !156, i32 21, i32 0, i32 3} ; [ DW_TAG_lexical_block ] [/home/pspacek/pkg/klee/git/build/runtime/Intrinsic//home/pspacek/pkg/klee/git/runtime/Intrinsic/memmove.c] | |
!163 = metadata !{i32 24, i32 0, metadata !162, null} | |
!164 = metadata !{i32 23, i32 0, metadata !162, null} | |
!165 = metadata !{metadata !165, metadata !148, metadata !149} | |
!166 = metadata !{metadata !166, metadata !148, metadata !149} | |
!167 = metadata !{i32 28, i32 0, metadata !71, null} | |
!168 = metadata !{i32 15, i32 0, metadata !85, null} | |
!169 = metadata !{i32 16, i32 0, metadata !85, null} | |
!170 = metadata !{metadata !170, metadata !148, metadata !149} | |
!171 = metadata !{metadata !171, metadata !148, metadata !149} | |
!172 = metadata !{i32 17, i32 0, metadata !85, null} | |
!173 = metadata !{i32 13, i32 0, metadata !99, null} | |
!174 = metadata !{i32 14, i32 0, metadata !99, null} | |
!175 = metadata !{i32 15, i32 0, metadata !99, null} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ ktest-tool test000002.ktest --write-ints | |
ktest file : 'test000002.ktest' | |
args : ['add-sym.bc'] | |
num objects: 2 | |
object 0: name: 'a' | |
object 0: size: 4 | |
object 0: data: 124 | |
object 1: name: 'b' | |
object 1: size: 4 | |
object 1: data: -2147442176 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
KLEE: ERROR: (location information missing) ASSERTION FAIL: f1(a, b) == f2(a, b) | |
KLEE: NOTE: now ignoring this error at this location |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Error: ASSERTION FAIL: f1(a, b) == f2(a, b) | |
Stack: | |
#000000096 in main (argc=1, argv=10982128) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment