Opened 5 years ago

Closed 5 years ago

#114 closed defect (worksforme)

divine check fails with "cannot enter kernel mode here"

Reported by: John Lång Owned by: mornfall
Priority: major Milestone: 4.4
Component: other Keywords:
Cc: John Lång

Description

When I'm trying to check my models with DIVINE 4.4.2 (after building them first with the same version), I get an error message that I don't understand. I've tried multiple models, and they all fail with the same message. I'll attach sample output from one of my models. I think this problem should be also reproducible with a model that I previously investigated with DIVINE 4.1.20+2018.12.17 and submitted into a permanent archive: ​https://zenodo.org/record/3258225

Attachments (1)

output.txt​ (1.3 KB) - added by John Lång 5 years ago.

Download all attachments as: .zip

Change History (4)

Changed 5 years ago by John Lång

Attachment: output.txt​ added

comment:1 Changed 5 years ago by John Lång

It seems to me that something goes wrong whenever I create a thread.

comment:2 Changed 5 years ago by John Lång

Cc: John Lång added

comment:3 Changed 5 years ago by mornfall

Resolution: → worksforme
Status: new → closed

I believe this is resolved: the problem was a change in the semantics of skipcfl (vs local_skipcfl) where the latter was intended (and skipcfl used to behave that way in older versions).

Note: See TracTickets for help on using tickets.