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

2022-03-09 Thread Cristian Cadar

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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


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

2022-03-04 Thread Sandip Ghosal
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev