BritikovKI / aeval

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

[FEAT]: TGNonlin should support byte operations #9

Closed BritikovKI closed 7 months ago

BritikovKI commented 8 months ago

Feature request

Feature Description

Currently we can't support any contracts that do even the simplest operations with bytes and bitvectors, we should add the capabilities of tgnonlin to handle them.

Required changes

Requirements which implemented feature should support:

  1. (_ int2bv 256) should be supported by the marshaling/unmarshaling
  2. int2bv can be encoded as UF possibly

Examples

This is the industrial contract which we can't currently support due to the lack of int2bv:

This is the minimized version of this problem:

Additional context

-

BritikovKI commented 7 months ago

Fixed