[klee-dev] How to solve "silently concretizing" in Klee

[Peidong Chen]

KLEE: WARNING ONCE: silently concretizing (reason: floating point)
expression (ReadLSB w32 0 a) to value
0 (/home/admin-ubuntu/Development/Project/Klee/struct-test1.c:17)

This is my source code:

#include "klee/klee.h"
#include "stdio.h"
#include <stdlib.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;
      a = (simple_struct*)malloc(sizeof(*a));
        klee_make_symbolic(a, sizeof(*a), "a");
          return struct_test1(a);
}
-------------- next part --------------
HTML attachment scrubbed and removed