Opened 5 years ago

Closed 5 years ago

#65 closed defect (invalid)

Error message in symbolic mode

Reported by: otis01329 Owned by: mornfall
Priority: major Milestone: 4.3
Component: other Keywords:

Description (last modified by mornfall)

In the symbolic mode using the divine, I have encountered the following error problem.

FAULT: undefined pointer dereference: [global* 0 2 uun]
[0] FATAL: memory error in userspace

What program will cause this error, can you provide me with the code that will cause this kind of error?

Because the program is very large, I can't provide my program. Sorry.

Change History (3)

comment:1 Changed 5 years ago by mornfall

Description: modified (diff)
Resolution: invalid
Status: newclosed

A program which gives the same error as you see would be the following. If you think the error is wrong or a problem with divine, you will need to provide more info, at minimum the backtrace(s) that follow the error message you got.

int main()
    char *a;
    return a[2];

comment:2 Changed 5 years ago by otis01329

Resolution: invalid
Status: closedreopened

I put the report of the divine4 output in the cloud.

Thank you for your help.

Last edited 5 years ago by otis01329 (previous) (diff)

comment:3 Changed 5 years ago by mornfall

Resolution: invalid
Status: reopenedclosed

While this does look like a real problem in the support code for symbolic data representation, we can't really fix the issue without a proper test case. On the other hand, the code evolves quite quickly and the problem might have been already fixed.

Note: See TracTickets for help on using tickets.