Opened 4 months ago

Closed 2 days ago

#65 closed defect (invalid)

Error message in symbolic mode

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

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 4 months 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 4 months ago by otis01329

Resolution: invalid
Status: closedreopened

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

https://drive.google.com/file/d/1M8OXKkddAFEamPJXvGQYcVPH7itid53m/view?usp=sharing

Thank you for your help.

Last edited 4 months ago by otis01329 (previous) (diff)

comment:3 Changed 2 days 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.