search

BritikovKI / aeval

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

[BUG]: SegFault while trying get_set() #10

Open BritikovKI opened 8 months ago

BritikovKI commented 8 months ago

Bug report

Bug description

An execution of tgnonlin on some encodings may cause segfault due to the exception in the get_set function.

To reproduce

For a following file:

Run command: tgnonlin --keys contract_Ownable_75:state,msg.value,msg.sender,initialOwner^owner__60:state,msg.value,msg.sender ./Ownable_updated.smt2

Run command:

Another example:

Run command: tgnonlin --keys contract_Ownable_75:state,msg.value,msg.sender,initialOwner^owner__60:state,msg.value,msg.sender ./Ownable_updated.smt2

TGNonlin follows this behavior:

  1. NonlinCHCSolver is executed until line 564
  2. On the call t->get_set, get_set function recurres
  3. Recursion ends up in the SegFault(as for some specific node there are no children)

Expected behaviour

File is processed correctly.