Your code seems to have some problems, although I don't know how they
affect the Klee operation. I compiled your code with my LLVM 2.6
installation, and it resulted:
define i32 @main(i32 %argc, i8** %argv) nounwind {
entry:
%argc_addr = alloca i32 ; <i32*> [#uses=2]
%argv_addr = alloca i8** ; <i8***> [#uses=2]
%retval = alloca i32 ; <i32*> [#uses=2]
%c = alloca i32 ; <i32*> [#uses=3]
%0 = alloca i32 ; <i32*> [#uses=3]
%"alloca point" = bitcast i32 0 to i32 ; <i32> [#uses=0]
call void @llvm.dbg.func.start({ }* bitcast
(%llvm.dbg.subprogram.type* @llvm.dbg.subprogram to { }*))
%1 = bitcast i32* %argc_addr to { }* ; <{ }*> [#uses=1]
call void @llvm.dbg.declare({ }* %1, { }* bitcast
(%llvm.dbg.variable.type* @llvm.dbg.variable to { }*))
store i32 %argc, i32* %argc_addr
%2 = bitcast i8*** %argv_addr to { }* ; <{ }*> [#uses=1]
call void @llvm.dbg.declare({ }* %2, { }* bitcast
(%llvm.dbg.variable.type* @llvm.dbg.variable10 to { }*))
store i8** %argv, i8*** %argv_addr
%3 = bitcast i32* %c to { }* ; <{ }*> [#uses=1]
call void @llvm.dbg.declare({ }* %3, { }* bitcast
(%llvm.dbg.variable.type* @llvm.dbg.variable12 to { }*))
call void @llvm.dbg.stoppoint(i32 4, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
%c1 = bitcast i32* %c to i8* ; <i8*> [#uses=1]
call void @klee_make_symbolic(i8* %c1, i64 4, i8* getelementptr
inbounds ([2 x i8]* @.str13, i64 0, i64 0)) nounwind
call void @llvm.dbg.stoppoint(i32 5, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
%4 = load i32* %c, align 4 ; <i32> [#uses=1]
%5 = icmp sgt i32 %4, 10 ; <i1> [#uses=1]
br i1 %5, label %bb, label %bb2
; No predecessors!
call void @llvm.dbg.stoppoint(i32 5, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
br label %bb
bb: ; preds = %6, %entry
call void @llvm.dbg.stoppoint(i32 6, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
store i32 1, i32* %0, align 4
br label %bb3
; No predecessors!
call void @llvm.dbg.stoppoint(i32 6, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
br label %bb2
bb2: ; preds = %7, %entry
call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
store i32 0, i32* %0, align 4
br label %bb3
bb3: ; preds = %bb2, %bb
call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
%8 = load i32* %0, align 4 ; <i32> [#uses=1]
store i32 %8, i32* %retval, align 4
br label %return
return: ; preds = %bb3
%retval4 = load i32* %retval ; <i32> [#uses=1]
call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
(%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
call void @llvm.dbg.region.end({ }* bitcast
(%llvm.dbg.subprogram.type* @llvm.dbg.subprogram to { }*))
ret i32 %retval4
}
You can see that the llvm.dbg.* calls do not have the "metadata
<badref>", but some valid parameters instead.
In any case, I attached in this message the test.o file that works for
me (it generates 2 paths with Klee). You should try it out and see if
it works with your Klee setup, as well. If it does, then there is a
problem with the way you set up LLVM on your machine.
Stefan
On Thu, May 20, 2010 at 9:17 PM, Heinz Riener <hriener at student.tugraz.at>
wrote:
> Hi Stefan,
>
> for me the llvm code looks correct: ?There is an icmp instruction and one
> way from entry over bb to bb3 and one way from entry over bb2 to bb3.
>
> $ cat test.o.ll
> ...
> define i32 @main(i32 %argc, i8** %argv) nounwind {
> entry:
> ?%argc_addr = alloca i32 ? ? ? ? ? ? ? ? ? ? ? ? ; <i32*> [#uses=1]
> ?%argv_addr = alloca i8** ? ? ? ? ? ? ? ? ? ? ? ?; <i8***> [#uses=1]
> ?%retval = alloca i32 ? ? ? ? ? ? ? ? ? ? ? ? ? ?; <i32*> [#uses=2]
> ?%0 = alloca i32 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ; <i32*> [#uses=3]
> ?%c = alloca i32 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ; <i32*> [#uses=2]
> ?%"alloca point" = bitcast i32 0 to i32 ? ? ? ? ?; <i32> [#uses=0]
> ?call void @llvm.dbg.declare(metadata <badref>, metadata !0)
> ?store i32 %argc, i32* %argc_addr
> ?call void @llvm.dbg.declare(metadata <badref>, metadata !9)
> ?store i8** %argv, i8*** %argv_addr
> ?call void @llvm.dbg.declare(metadata <badref>, metadata !10)
> ?%c1 = bitcast i32* %c to i8* ? ? ? ? ? ? ? ? ? ?; <i8*> [#uses=1]
> ?call void @klee_make_symbolic(i8* %c1, i32 4, i8* getelementptr inbounds
> ([2 x i8]* @.str, i32 0, i32 0)) nounwind
> ?%1 = load i32* %c, align 4 ? ? ? ? ? ? ? ? ? ? ?; <i32> [#uses=1]
> ?%2 = icmp sgt i32 %1, 10 ? ? ? ? ? ? ? ? ? ? ? ?; <i1> [#uses=1]
> ?br i1 %2, label %bb, label %bb2
>
> bb: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ; preds = %entry
> ?store i32 1, i32* %0, align 4
> ?br label %bb3
>
> bb2: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?; preds = %entry
> ?store i32 0, i32* %0, align 4
> ?br label %bb3
>
> bb3: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?; preds = %bb2, %bb
> ?%3 = load i32* %0, align 4 ? ? ? ? ? ? ? ? ? ? ?; <i32> [#uses=1]
> ?store i32 %3, i32* %retval, align 4
> ?br label %return
>
> return: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ; preds = %bb3
> ?%retval4 = load i32* %retval ? ? ? ? ? ? ? ? ? ?; <i32> [#uses=1]
> ?ret i32 %retval4
> }
> ...
>
> Heinz
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.o
Type: application/x-object
Size: 1908 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100520/2961d27a/attachment.bin
