GaloisInc / what4

Symbolic formula representation and solver interaction library
155 stars 13 forks source link

Tests for the preservation of abstract values #249

Open langston-barrett opened 11 months ago

langston-barrett commented 11 months ago

Inspired by #248, I propose we add tests that demonstrate that the IsExprBuilder methods of ExprBuilder preserve abstract values. One option would be to randomly generate expressions over a single base type (e.g., trees of string operations), then interpret them directly in the abstract domain and also via ExprBuilder methods, and assert that the abstract value of the latter refines the former.