search

BritikovKI / aeval

ADT-processing for test generation
Other
0 stars 0 forks source link

[BUG]: In some cases when analysing CHCs index_cycle_chc is empty #7

Open BritikovKI opened 8 months ago

BritikovKI commented 8 months ago

Bug report

Bug description

When running a chc-encoded version of three contracts, connected in inheritance chain, it is possible that tg-nonlin will fail due to the fact that it can't fund any index_cycles.

To reproduce

For following files:

TGNonlin follows this behavior:

  1. Tries to find any index_cycles (lines 564-575 of HornNonlin.hpp), fails to find any
  2. Reverts at line 577

Expected behaviour

Based on the CHC analysis it should be able to find at least some cases, where CHC destination is also a source for some other CHC predicate, even for the case when there are no functions and only constructors in the contract.

Files or input data

The running comand:

tgnonlin --keys contract_Cv1_131:state,msg.value,msg.sender constructor_state_variable_init_updated.smt2

Additional context

Same problem holds for a set of constructor_state_variable benchmarks:

I suppose it is connected with a fact that there are no functions in the contracts.

BritikovKI commented 7 months ago

This happens because there are no public functions in the contract, so there is nothing to test(except the constructor).

I suppose it makes sense to not test this funcs, but feature needed to test contracts only with constructors!