Skip to content

Commit

Permalink
fix: markdown links (#1377)
Browse files Browse the repository at this point in the history
  • Loading branch information
xldenis authored Feb 23, 2025
2 parents 340537d + 0089f3f commit 5b5f38c
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 10 deletions.
4 changes: 2 additions & 2 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Follow the instructions provided in the [README](./README.md). This will provide

## 2.1. UI Tests

The UI tests are used to validate the translation of Creusot. They can be found in `creusot/tests/should_fail` and `creusot/tests/should_suceed`.
The UI tests are used to validate the translation of Creusot. They can be found in `tests/should_fail` and `tests/should_suceed`.
Ideally, each test includes a comment specifying the property or feature being checked.
To validate the translation one can run `cargo test --test ui`, or to run only a subset of tests run `cargo test --test ui "pattern"`.

Expand All @@ -19,7 +19,7 @@ When contributing or updating tests, we ask that you minimize avoidable warnings
The warnings and errors of each test are recorded in an accompanying `stderr` file if any were present.

The `ui` test also runs the Creusot translation on `creusot-contracts`.
The result is located at `creusot/tests/creusot-contracts/creusot-contracts.coma`.
The result is located at `tests/creusot-contracts/creusot-contracts.coma`.
To run the translation only on `creusot-contracts`, use a pattern that matches nothing, like `cargo test --test ui qq`

# 3. Verifying proofs
Expand Down
4 changes: 2 additions & 2 deletions HACKING.md
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,9 @@ Additional useful parameters, to avoid replaying *every* proof in development:
## Inspecting/fixing the proof of a test

If the proof of a test is broken (e.g.
`creusot/tests/should_succeed/cell/01.rs`), launch the why3 ide with `./ide`:
`tests/should_succeed/cell/01.rs`), launch the why3 ide with `./ide`:
```
./ide creusot/tests/should_succeed/cell/01
./ide tests/should_succeed/cell/01
```

## Calling why3 (and why3_tools, etc): shell environment setup
Expand Down
12 changes: 6 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,13 @@ If you would like to cite Creusot in academic contexts, we encourage you to use

To get an idea of what verifying a program with Creusot looks like, we encourage you to take a look at some of our test suite:

- [Zeroing out a vector](creusot/tests/should_succeed/vector/01.rs)
- [Binary search on Vectors](creusot/tests/should_succeed/vector/04_binary_search.rs)
- [Sorting a vector](creusot/tests/should_succeed/vector/02_gnome.rs)
- [IterMut](creusot/tests/should_succeed/iterators/02_iter_mut.rs)
- [Normalizing If-Then-Else Expressions](creusot/tests/should_succeed/ite_normalize.rs)
- [Zeroing out a vector](tests/should_succeed/vector/01.rs)
- [Binary search on Vectors](tests/should_succeed/vector/04_binary_search.rs)
- [Sorting a vector](tests/should_succeed/vector/02_gnome.rs)
- [IterMut](tests/should_succeed/iterators/02_iter_mut.rs)
- [Normalizing If-Then-Else Expressions](tests/should_succeed/ite_normalize.rs)

More examples are found in [creusot/tests/should_succeed](creusot/tests/should_succeed).
More examples are found in [tests/should_succeed](tests/should_succeed).

## Projects built with Creusot

Expand Down

0 comments on commit 5b5f38c

Please sign in to comment.