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

[Cristian Cadar]

KLEE concretizes that value because it lacks support for symbolic 
floating point.

Best,
Cristian

On 25/01/15 21:05, Peidong Chen wrote:
> 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);
> }
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>