Bug #7271
opencrash in ldv-challenges as signal 6: what(): map::at
70%
Description
File:
~/hi-bench/challenge-bench/sv-comp17/c/ldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-ethernet-via-via-velocity_true-unreach-call.cil.c
---------------------------
How to run:
./hifrog --sum-theoref --unwind 10 file.c
---------------------------
Error msg:
Use QF_UF logic.
terminate called after throwing an instance of 'std::out_of_range'
what(): map::at
Command terminated by signal 6
initial observation:
the error is caused by hifrog asking for a goto function which is not known. There is a line of code in the program:
asm volatile ("lfence": : : "memory");
And perhaps it could come from there.
Updated by Karine Even Mendoza over 6 years ago
- Status changed from New to Feedback
- Assignee set to Sepideh Asadi
- % Done changed from 0 to 70
I added back the asm_ build-in cprover functions, not sure it is the right thing to do, it can be that we will have performance issues.
Currently it doesn't crash.
Updated by Karine Even Mendoza over 6 years ago
Currently the issue is as bug #7272, shall we unify the reports?