KLEE demonstration program

add-sym.c

#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;
}

add.c

#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;
}

assembly.ll

; 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}

ktest-tool test000002.ktest --write-ints

$ 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

messages.txt

KLEE: ERROR: (location information missing) ASSERTION FAIL: f1(a, b) == f2(a, b)
KLEE: NOTE: now ignoring this error at this location

test000002.assert.err

Error: ASSERTION FAIL: f1(a, b) == f2(a, b)
Stack:
        #000000096 in main (argc=1, argv=10982128)