hifrog

=========================
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.