[klee-dev] about struct klee test

[Dingbao Xie]

You made a mistake when using klee_make_symbolic.
>From your code, I assume that you want to make *a symbolic not a.

Try to use the following code:

int main() {
  simple_struct *a;
  a = (simple_struct*)malloc(sizeof(*a));
  klee_make_symbolic(a, sizeof(*a), "a");
  return struct_test1(a);
}

On Wed, Jan 21, 2015 at 3:25 PM, Peidong Chen <peidong01 at gmail.com> wrote:

> 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?
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>


-- 
Dingbao Xie
-------------- next part --------------
HTML attachment scrubbed and removed