refinedc frontend should be more flexible about placement of verification files
From #37 (closed):
Running the README instructions, I figured simply naming it
test.c would be OK, but I got the following error:
refinedc check test.c refinedc: internal error, uncaught exception: (Invalid_argument "String.sub / Bytes.sub") Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45 Called from Stdlib__string.sub in file "string.ml" (inlined), line 47, characters 2-23 Called from Dune__exe__Extra.Filename.relative_path in file "frontend/extra.ml", line 105, characters 6-62 Called from Dune__exe__Main.run in file "frontend/main.ml", line 163, characters 28-70 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 25, characters 19-24 Called from Cmdliner.Term.run in file "cmdliner.ml", line 117, characters 32-39 make: *** [Makefile:9: check] Error 125
src and moving
test.c into it fixed the issue, but the original error was very difficult to reason about (would have been impossible to understand had I not been following the readme) and seems like a strange limitation to have in the first place.
It's certainly going to cause some headache for contributors to our project - at this point, I will have to wrap the entire verification task inside a Dockerfile, which is pretty unfortunate DX given that our codebase does not follow the
src pattern and Docker is a hefty, intrusive and brittle dependency. Further, even if it did follow the
src hierarchy, it would add some cruft to the directory hierarchy. I would much rather specify (ideally from the command line) where directories should be placed/checked, and which files I'm interested in verifying.