Skip to content

Commit

Permalink
Update readme.md
Browse files Browse the repository at this point in the history
Add information for using Mill with Windows
  • Loading branch information
l-kent authored Jul 22, 2024
1 parent 8135d0c commit 75603e0
Showing 1 changed file with 19 additions and 6 deletions.
25 changes: 19 additions & 6 deletions readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,21 @@ Boogie program verifier finished with 4 verified, 0 errors

The tool takes as inputs either a BAP ADT file (here denoted with `.adt`) or a `.gts` file produced by [gtirb-semantics](https://github.com/UQ-PAC/gtirb-semantics), as well as a file containing the output of readelf (here denoted with `.relf`), both created from the same AArch64/ARM64 binary, and outputs a semantically equivalent .bpl Boogie-language source file. The default output file is `boogie_out.bpl`, but the output location can be specified.

To build and run the tool using sbt, use the following command:
To build and run the tool use one of the the following commands:

`sbt "run --input file.{adt, gts} --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.

or mill:

`mill run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]`.
sbt:
```
sbt "run --input file.{adt, gts} --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"
```
mill (Mac OS X / Linux):
```
./mill run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]
```
mill (Windows):
```
./mill.bat run --input file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]
```
The output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.

#### Usage

Expand Down Expand Up @@ -82,9 +90,14 @@ See [docs/development](docs/development)
2. Install [boogie](/docs/development/tool-installation.md)
3. To a single system test case :

Mac OS X / Linux:
```
./mill test.testOnly '*SystemTests*' -- -z secret_write -z secret_write
```
Windows:
```
./mill.bat test.testOnly '*SystemTests*' -- -z secret_write -z secret_write
```

## Open Source License

Expand Down

0 comments on commit 75603e0

Please sign in to comment.