Project

General

Profile

Actions
Copy link

Bug #5107

open

inconsistency in directory: product-lines

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

Status:
New
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
02/05/2017
Due date:
% Done:

10%

Estimated time:

Description

HiFROG:
minepump_spec4_product41_false-unreach-call.cil.c UNSAT with CUSTOM 6.229 s

CBMC:
minepump_spec4_product41_false-unreach-call.cil.c SAT 1.6 s

Actions
Copy link
 #1

Updated by Karine Even Mendoza over 7 years ago

fails up to 5, wonder what if the unwind is larger...

Actions
Copy link
 #2

Updated by Karine Even Mendoza over 7 years ago

  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 10
=========================
Results from CBMC:
  • Results:
    [__automaton_fail.assertion.1] : FAILURE
    [__utac__get_this_arg.assertion.1] assertion i > 0 && i <= this->argsCount: SUCCESS
    [__utac__get_this_arg.assertion.2] assertion i > 0 && i <= this->argsCount: SUCCESS
    [__utac__get_this_argtype.assertion.1] assertion i > 0 && i <= this->argsCount: SUCCESS
    [__utac__get_this_argtype.assertion.2] assertion i > 0 && i <= this->argsCount: SUCCESS
  • 1 of 5 failed (2 iterations)
    VERIFICATION FAILED
    karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./../cbmc/cbmc ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c --unwind 3

Claims are:
Generic Property Instrumentation
Property __automaton_fail.assertion.1:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 211 function __automaton_fail
assertion
FALSE

Property _utac_get_this_arg.assertion.1:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 520 function _utac_get_this_arg
assertion i > 0 && i <= this->argsCount
i > 0

Property _utac_get_this_arg.assertion.2:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 513 function _utac_get_this_arg
assertion i > 0 && i <= this->argsCount
i <= __cil_tmp6

Property _utac_get_this_argtype.assertion.1:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 566 function _utac_get_this_argtype
assertion i > 0 && i <= this->argsCount
i > 0

Property _utac_get_this_argtype.assertion.2:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 559 function _utac_get_this_argtype
assertion i > 0 && i <= this->argsCount
i <= __cil_tmp6

=====================
Results from HiFrog:

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 33.999

Checked Assertion:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/product-lines/minepump_spec4_product41_false-unreach-call.cil.c line 211 function __automaton_fail
assertion
FALSE
#X: Done.
karinek@kar

The rest of the assertions aren't reachable. Check why.

Actions
Copy link

Also available in: Atom PDF