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

JVMSetup errors don't print source location #1021

Closed
brianhuffman opened this issue Jan 20, 2021 · 1 comment · Fixed by #1075
Closed

JVMSetup errors don't print source location #1021

brianhuffman opened this issue Jan 20, 2021 · 1 comment · Fixed by #1075
Assignees
@brianhuffman
Labels
easy Issues that are expected to be easy to resolve and might therefore be good for new contributors subsystem: crucible-jvm Issues related to Java verification with crucible-jvm

Comments

@brianhuffman
Copy link
Contributor

brianhuffman commented Jan 20, 2021 •
edited
Loading

As an example, here's the saw output if you get the argument list wrong on a jvm_execute_func:

[02:31:22.223] Loading file "/Users/huffman/Work/saw-script/examples/java/fields.saw"
[02:31:22.292] jvm_execute_func: Argument type mismatch
Argument position: 0
Expected type: Fields
Given type: int

I would expect the error message to be printed out with a full saw-script stack trace, with source location information.

This probably has something to do with exception handlers and the custom exception type that JVMSetup uses.
@brianhuffman brianhuffman changed the title JVMSetup errors don JVMSetup errors don't print source location Jan 20, 2021
@brianhuffman brianhuffman reopened this Jan 20, 2021
@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Jan 20, 2021
@brianhuffman brianhuffman self-assigned this Feb 12, 2021
@brianhuffman brianhuffman added the easy Issues that are expected to be easy to resolve and might therefore be good for new contributors label Feb 12, 2021
brianhuffman pushed a commit that referenced this issue Feb 15, 2021
Embed JVMSetupError inside TopLevelException datatype.
9f71feb 
This means that JVMSetupError exceptions can now be caught by
the standard TopLevelException handlers, and get shown with
the expected stack traces in the saw-script REPL.

This is done using a new existentially-typed `SomeTopLevelException`
constructor, as recommended by the Control.Exception documentation.

Fixes #1021.
@brianhuffman brianhuffman mentioned this issue Feb 15, 2021
Merged
@brianhuffman
Copy link
Contributor Author

With #1075, running the test_jvm_setup_errors integration tests shows that the expected failure messages now include a stack trace with location information.

brianhuffman pushed a commit that referenced this issue Feb 17, 2021
Embed JVMSetupError inside TopLevelException datatype.
3960578 
This means that JVMSetupError exceptions can now be caught by
the standard TopLevelException handlers, and get shown with
the expected stack traces in the saw-script REPL.

This is done using a new existentially-typed `SomeTopLevelException`
constructor, as recommended by the Control.Exception documentation.

Fixes #1021.
brianhuffman pushed a commit that referenced this issue Feb 23, 2021
Embed JVMSetupError inside TopLevelException datatype.
090b21c 
This means that JVMSetupError exceptions can now be caught by
the standard TopLevelException handlers, and get shown with
the expected stack traces in the saw-script REPL.

This is done using a new existentially-typed `SomeTopLevelException`
constructor, as recommended by the Control.Exception documentation.

Fixes #1021.
brianhuffman pushed a commit that referenced this issue Feb 25, 2021
Embed JVMSetupError inside TopLevelException datatype.
a47c087 
This means that JVMSetupError exceptions can now be caught by
the standard TopLevelException handlers, and get shown with
the expected stack traces in the saw-script REPL.

This is done using a new existentially-typed `SomeTopLevelException`
constructor, as recommended by the Control.Exception documentation.

Fixes #1021.
@mergify mergify bot closed this as completed in #1075 Mar 1, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@brianhuffman brianhuffman

Labels
easy Issues that are expected to be easy to resolve and might therefore be good for new contributors subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Embed JVMSetupError inside TopLevelException datatype. GaloisInc/saw-script
1 participant
@brianhuffman