[klee-dev] Please help me figure out what is happening in External Dispatcher

Dan Liew dan at su-root.co.uk
Fri Apr 10 20:35:29 BST 2015


Hi,

On 10 April 2015 at 18:28, Chace Clark <chace3 at tamu.edu> wrote:
> I am trying to figure out why some of my calls to external functions are
> producing odd behaviors. Its like some functions are leaving things on the
> stack.
> For example when I run my version of KLEE on:
>
> void main(){
>   printf("hi\n");
>   int haspwd = strncmp("a", "PWD=", 4)==0;
>   printf("bye\n");
> }

I can't reproduce this issue

```
$ clang -c -emit-llvm foo.c -o foo.bc
foo.c:1:1: warning: return type of 'main' is not 'int' [-Wmain-return-type]
void main(){
^
foo.c:1:1: note: change return type to 'int'
void main(){
^~~~
int
foo.c:2:3: warning: implicitly declaring library function 'printf'
with type 'int (const char *, ...)'
  printf("hi\n");
  ^
foo.c:2:3: note: please include the header <stdio.h> or explicitly
provide a declaration for 'printf'
foo.c:3:16: warning: implicitly declaring library function 'strncmp'
with type 'int (const char *, const char *, unsigned long)'
  int haspwd = strncmp("a", "PWD=", 4)==0;
               ^
foo.c:3:16: note: please include the header <string.h> or explicitly
provide a declaration for 'strncmp'
3 warnings generated.

$ klee foo.bc
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: strncmp
KLEE: WARNING ONCE: calling external: printf(42827920)
hi
KLEE: WARNING ONCE: calling external: strncmp(42746256, 42651584, 4)
bye

KLEE: done: total instructions = 8
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
```



More information about the klee-dev mailing list