Project

General

Profile

Bug #7271

crash in ldv-challenges as signal 6: what(): map::at

Added by Sepideh Asadi about 1 year ago. Updated about 1 year ago.

Status:
Feedback
Priority:
Normal
Assignee:
Start date:
03/05/2018
Due date:
% Done:

70%

Estimated time:

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.

History

#1 Updated by Karine Even Mendoza about 1 year 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.

#2 Updated by Karine Even Mendoza about 1 year ago

Currently the issue is as bug #7272, shall we unify the reports?

Also available in: Atom PDF