On Mon, Dec 5, 2011 at 10:34 PM, Paul Marinescu <
[email protected]> wrote:
> I didn't have time to check this, but it should work by adding a call to
> klee_define_fixed_object(<my ptr>, <my ptr size>) in the program, somewhere
> before <my ptr> is dereferenced. See lib/Core/SpecialFunctionHandler.cpp
> for the intrinsic implementation.
>
> Paul
>
It somewhat worked, but not as i excepted. Here is <my ptr>, which i'm
putting into bitcode:
int * testVar=new int;
*testVar=88;
And here is resulting bitcode:
define i32 @main() nounwind uwtable {
entry:
%retval = alloca i32, align 4
%myPtr = alloca i32*, align 8
store i32 0, i32* %retval
store i64 34397700356, i32** %myPtr, align 8
%0 = load i32** %myPtr, align 8
%1 = bitcast i32* %0 to i8*
call void @klee_define_fixed_object(i8* %1, i64 4)
%2 = load i32** %myPtr, align 8
call void @foo(i32* %2)
ret i32 0
}
That 34397700356 in store is value of testVar;
Now, in @foo() i call printf("%d", *myptr), and here is KLEE's output:
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: calling external: printf(34397593784, 0)
0
Why is it 0 instead of 88?
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
