Project

General

Profile

Actions
Copy link

Bug #7276

open

crash on busybox categories; Ideally we should return UNSUPPORTED!

Added by Sepideh Asadi over 6 years ago. Updated over 6 years ago.

Status:
Resolved
Priority:
Normal
Assignee:
Martin Blicha
Start date:
07/05/2018
Due date:
% Done:

0%

Estimated time:

Description

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.c

Verification was not successful, here is the last few lines: ...

Total number of claims in program...(1).
; Warning: disabling SATElite preprocessing to track proof
Use QF_UF logic.

---------checking claim # 1 ---------
; Warning: disabling SATElite preprocessing to track proof
hifrog: /home/asadis/new-hifrog/hifrog/trunk/cprover/src/funfrog/symex_assertion_sum.cpp:1695: ssa_exprt symex_assertion_sumt::get_next_version(const symbolt&): Assertion `state.level2.current_names.find(ssa_l1_identifier) != state.level2.current_names.end()' failed.
  • INLINING function: __CPROVER_initialize
  • INLINING function: main
    Processing a deferred function: __CPROVER_initialize
    Processing a deferred function: main
    Command terminated by signal 6
    real 4.12

Note: Busybox is full of pointer, heap manipulation,...as sated in the svcomp webpage this category aims to represent verification tasks from real software systems.

Note2: This crash happens in 9 benchmarks out of 40.

Actions
Copy link
 #1

Updated by Karine Even Mendoza over 6 years ago

  • Assignee set to Martin Blicha
  • Priority changed from Low to Normal

It is a bug in the creation of the SSA symbols. Somehow a symbol in modified_globals container isn't in the cprover's tables.
It is a program variable, not a fabricated one.

Actions
Copy link
 #2

Updated by Martin Blicha over 6 years ago

  • Status changed from New to Resolved

Previously we were expecting to see a declaration of all symbols, but there are symbols that do not have declarations, like extern variables.
Now, we let the state before symex know about such variables before-hand. See git commit f8cc89bc

Actions
Copy link

Also available in: Atom PDF