Skip to content

Bug: documentation for --dest and --dest-dir does not match actual behavior #1011

@protz

Description

@protz

When one of the arguments passed to cargo is --manifest-path, the --dest-dir and --dest options no longer behave according to the documentation.

Specifically, charon --dest-file foo.llbc -- --manifest-path path/to/Cargo.toml creates path/to/foo.llbc even though the option documentation states that ./foo.llbc will be created.

My preferred fix would be for the options to behave as stated in the documentation, /even when/ --manifest-path is used, so as to avoid running an additional mv in the Makefile (not to mention that if the proofs are in directory that's separate from the main code repository, it's not super clean to write build outputs outside of the proof project)

Metadata

Metadata

Assignees

No one assigned

    Labels

    C-bugA bug in charon

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions