search

cuter-testing / cuter

A concolic testing tool for the Erlang functional programming language.
GNU General Public License v3.0
211 stars 20 forks source link

Solver error in ets:file2tab #120

Closed ioolkos closed 7 years ago

ioolkos commented 7 years ago

cuter ets file2tab '[filename]' --disable-pmatch (and also file2tab/2) leads to SOLVER ERRORS for me.

Please tell me if it's NOT useful right now to report "small stuff" like that.

kostis commented 7 years ago

Your example is not particularly interesting as far as concolic execution is concerned, because you cannot really expect that CutEr will be able to come up with a file name that makes ets:file2tab/[1,2] crash. However, as I wrote in an other issue (#115), CutEr should not be crashing with SOLVER ERRORS, independently of whether the tests make sense or not. In this respect, we appreciate all reports of such cases you run across.

This particular SOLVER ERROR was due to the Erlang part of CutEr encoding references and pids and sending these to the SMT solver that does not yet know what to do with them. A pull request (#121), which is now merged on the master branch, comments out the encoding of references and pids for the time being. We will uncomment them when we come up with some way to handle these terms in the SMT solver.

Your example now works. Thanks for your report. We appreciate it.

ioolkos commented 7 years ago

@kostis thanks for the explanations and the fix! I'll happily open more issues, if I have findings and if I'm able to actually shrink them.