[klee-dev] Need help in making a structure pointer symbolic

Cristian Cadar c.cadar at imperial.ac.uk
Wed Mar 9 13:59:22 GMT 2022


Hi,

You can make pointers symbolic in KLEE, but this might not accomplish 
what you hope.  Making a pointer symbolic means it can refer to any 
address in memory, including invalid ones.

Best,
Cristian

On 04/03/2022 08:37, Sandip Ghosal wrote:
> Hello Everyone,
> 
> Can somebody help me to make a pointer to a structure symbolic?
> 
> For example, I have a linked list node, and I am trying to make the 
> pointer to the structure symbolic as follows:
> 
> struct Node{
>     int data;
>     struct Node *next;
> }
> 
> struct Node *node = NULL;
> 
> node = (struct Node*)malloc(sizeof(struct Node))
> 
> klee_make_symbolic(node, sizeof(struct Node *), "e1");
> 
> 
> Now what I understand is that Klee is not able to make memory address 
> symbolic probably because of infinite address space. Please let me know 
> if this is the limitation of Klee or there is some other way for making 
> a pointer variable symbolic.
> 
> Thanks in advance.
> 
> -- 
> Thanks & Regards
> Sandip Ghosal
> 
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



More information about the klee-dev mailing list