refinedc frontend should be more flexible about placement of verification files
From #37:
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
Creating 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.