Skip to content

Commit

Permalink
Update the README
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Dec 2, 2024
1 parent b0abe36 commit d6053c3
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,10 @@ If you run `make`, you will generate a documentation accessible from [`doc.html`

## Usage

You should first generate the serialized `.llbc` file by calling Charon from *inside*
(similarly to cargo) the crate you want to translate. **Important:** you should call
Charon with the `--hide-marker-traits` option: `charon --hide-marker-traits`.

The Aeneas binary is in `bin`; you can run: `./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE`,
where `LLBC_FILE` is an .llbc file generated by Charon.

Expand Down

0 comments on commit d6053c3

Please sign in to comment.