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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
