[klee-dev] about struct klee test

[Peidong Chen]

Hello,

I tried this .c file, but with many errors.

This is my file.
================================
struct_test1.c

#include "klee/klee.h"
#include "stdio.h"

typedef struct{
int n;
char c;
float f;
}simple_struct;

int struct_test1(simple_struct *s)
{
int ret;
simple_struct *p;
 if(s->c=='a'){
s->f=3.14*s->n*s->n;
ret=0;
}else if(s->c=='p'){
s->f=2*3.14*s->n;
ret=1;
}else {
s=p;
ret=2;
  }
  return ret;
}

int main() {
  simple_struct *a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return struct_test1(a);
}
==================================
Then, I compiled my file

$ clang-3.4 -c -g -emit-llvm -I
/home/admin-ubuntu/Development/Program/klee/include  struct-test1.c -o
struct-test1.o

And use klee

$ klee struct-test1.o

Then I see many errors:
*************************************
KLEE: ERROR: /home/admin-ubuntu/Development/Project/Klee/struct-test1.c:15:
memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/admin-ubuntu/Development/Project/Klee/struct-test1.c:16:
memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: silently concretizing (reason: floating point)
expression (ReadLSB w32 N0:(Extract w32 0 (Add w64 18446744073673478272
                                         (ReadLSB w64 0 a))) const_arr8) to
value 1914725481
(/home/admin-ubuntu/Development/Project/Klee/struct-test1.c:16)
KLEE: ERROR: /home/admin-ubuntu/Development/Project/Klee/struct-test1.c:16:
memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/admin-ubuntu/Development/Project/Klee/struct-test1.c:16:
memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/admin-ubuntu/Development/Project/Klee/struct-test1.c:19:
memory error: object read only
KLEE: NOTE: now ignoring this error at this location
***************************************

It says the memory error. Is that meaning that the way I treated with
pointers wrongly?
-------------- next part --------------
HTML attachment scrubbed and removed