Project

General

Profile

Bug #5104

Why CBMC does not verify many benchs but we do!!! Is there something wrong?

Added by Sepideh Asadi about 7 years ago. Updated almost 7 years ago.

Status:
Closed
Priority:
Low
Assignee:
Sepideh Asadi
Start date:
02/05/2017
Due date:
% Done:

0%

Estimated time:

Description

HiFROG:
ldv-challenges/linux-3.8-rc1-32_7a-drivers--net--ethernet--emulex--benet--be2net.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c UNSAT 0.476

CBMC:
ldv-challenges/linux-3.8-rc1-32_7a-drivers--net--ethernet--emulex--benet--be2net.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c NoResult Timeout

History

#1 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from New to Feedback
  • Assignee set to Sepideh Asadi
  • Priority changed from Normal to Low

shall unwind to 40, it seems like both of the tools iterates for ever...
Can you please have a look too?

It is not even getting to the stage of checking a claim since both tools run long in the parsing stage...

#2 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from Feedback to Closed

Also available in: Atom PDF