Symex - Githubissues

uuverifiers / eldarica

The Eldarica model checker

Other

80 stars 22 forks source link

Symex #50

Closed zafer-esen closed 1 year ago

zafer-esen commented 1 year ago

Symbolic execution framework. Currently implemented strategies using the framework:

Forward DFS - currently WIP, nonlinear clauses are not supported,
Forward BFS .

Also adds scalatest to the project with some unit tests for symbolic execution. Command for running the unit tests are added to GitHub workflows.

pruemmer commented 1 year ago

Thanks! This mostly looks ready to be merged, but here are two requests for changes:

the option -sym:n should be changed to receive textual arguments (maybe -sym:dfs and -sym:bfs); and there should be a default mode that can be enabled with just the option -sym
we should have some regression tests with symbolic execution. Maybe create a new sub-folder and copy over some of the examples from horn-smt-lib?

zafer-esen commented 1 year ago

Thanks for the feedback! 152185f implements the requested changes!

Regression tests for DFS are still missing, but added for BFS. There are unit tests for both BFS & DFS. The DFS implementation also needs more work, it cannot currently handle nonlinear clauses.