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.

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

Heapster: Prelude.head: empty list crash when invoking heapster_typecheck_mut_funs on empty list #2096

Open
RyanGlScott opened this issue Aug 21, 2024 · 0 comments
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Aug 21, 2024

Given the following C program SAW script:

// test.c
// test.saw
enable_experimental;
env <- heapster_init_env "test" "test.bc";
heapster_typecheck_mut_funs env [];

SAW will crash when attempting to run the program:

$ clang test.c -g -emit-llvm -c
$ ~/Software/saw-1.1/bin/saw test.saw
[12:41:17.884] Loading file "/home/ryanglscott/Documents/Hacking/Haskell/saw-script/test.saw"
[12:41:17.888] Stack trace:
"heapster_typecheck_mut_funs" (/home/ryanglscott/Documents/Hacking/Haskell/saw-script/test.saw:4:1-4:28)
Prelude.head: empty list

Either heapster_typecheck_mut_funs should be altered to accept an empty list, or it should fail with a better error message than Prelude.head: empty list (and the non-empty list requirement should be documented).

@RyanGlScott RyanGlScott added type: bug Issues reporting bugs or unexpected/unwanted behavior subsystem: heapster Issues specifically related to memory verification using Heapster labels Aug 21, 2024
RyanGlScott added a commit that referenced this issue Aug 21, 2024
Really, we should be throwing a proper error message here instead of throwing a
`panic`, and we should document the requirement that the list of mutually
recursive functions must be non-empty. That is left as future work (see #2096).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

1 participant