search

angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
275 stars 90 forks source link

String symbols abstraction explicitly not supported by z3 backend #319

Closed zwimer closed 1 year ago

zwimer commented 1 year ago

Not supported because z3 does not supported strings https://github.com/Z3Prover/z3/discussions/6443

github-actions[bot] commented 1 year ago

Unit Test Results

     94 files  +     84       94 suites  +84   1h 30m 14s :stopwatch: + 1h 29m 43s 1 401 tests +1 095  1 311 :heavy_check_mark: +1 065  90 :zzz: +30  0 :x: ±0  1 407 runs  +1 101  1 317 :heavy_check_mark: +1 071  90 :zzz: +30  0 :x: ±0 

Results for commit bbb9ecab. ± Comparison against base commit b279b77f.

:recycle: This comment has been updated with latest results.

zwimer commented 1 year ago

No point in CI right now; this will fail as the length was not set during string abstraction (a syntax error)

zwimer commented 1 year ago

This may not be possible as-is given: https://github.com/Z3Prover/z3/discussions/6443#discussioncomment-4081446

zwimer commented 1 year ago

Ping @ltfish

zwimer commented 1 year ago

I'm going to merge this; if it causes issues we can always revert; though if this causes issues, that probably indicates the thing with an issue is broken, not this.