rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
49 stars 27 forks source link

[CN] --state-file command-line argument doesn't understand `~` #339

Open PeterSewell opened 3 months ago

PeterSewell commented 3 months ago
~/repos/cerberus$ cn --state-file=~/tmp/cn-state.html  ~/tmp/foo.c
[1/1]: main
cn: internal error, uncaught exception:
    Sys_error("~/tmp/cn-state.html: No such file or directory")
    Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
    Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
    Called from Dune__exe__Report.make in file "backend/cn/report.ml", line 674, characters 11-28
    Called from Dune__exe__TypeErrors.report in file "backend/cn/typeErrors.ml", line 435, characters 18-85
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 214, characters 11-42
    Re-raised at Dune__exe__Main.main in file "backend/cn/main.ml", line 222, characters 6-71
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, characters 37-44
cp526 commented 3 months ago

Our argument syntax is different. Try without the =:

~/repos/cerberus$ cn --state-file ~/tmp/cn-state.html ~/tmp/foo.c

cp526 commented 3 months ago

Though we'll want CN to fail in a nicer way in the above situation.

PeterSewell commented 3 months ago

That works, but (a) indeed we'd want it to fail more nicely, and (b) it's not what the cn --help documents:

      --state-file=FILE
           file in which to output the state
cp526 commented 3 months ago

I take back what I said, I think I misunderstood the situation. I'll look into it