Skip to content

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

@BritikovKI

Description

@BritikovKI

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions