Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Solver error in ets:file2tab #120

Closed
ioolkos opened this issue Mar 14, 2017 · 2 comments
Closed

Solver error in ets:file2tab #120

ioolkos opened this issue Mar 14, 2017 · 2 comments

Comments

@ioolkos
Copy link

ioolkos commented Mar 14, 2017

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 added a commit that referenced this issue Mar 16, 2017
@kostis
Comment out encoding of refs and pids for the time being
b76e024 
Also comment out the corresponding tests until we decide what
is the proper way to handle these terms in the solver.

This fixes the SOLVER ERROR crash reported in #120.
@kostis kostis mentioned this issue Mar 16, 2017
Merged
@kostis
Copy link
Collaborator

kostis commented Mar 16, 2017 •
edited
Loading

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.

@kostis kostis closed this as completed Mar 16, 2017
kostis added a commit that referenced this issue Mar 16, 2017
@kostis
Comment out encoding of refs and pids for the time being (#121)
abb7a11 
Also comment out the corresponding tests until we decide what
is the proper way to handle these terms in the solver.

This fixes the SOLVER ERROR crash reported in #120.
@ioolkos
Copy link
Author

ioolkos commented Mar 17, 2017

@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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@kostis @ioolkos