Skip to content

Commit

Permalink
update RunMain with Rust error
Browse files Browse the repository at this point in the history
  • Loading branch information
RitvikKapila committed Dec 17, 2024
1 parent ead7d3b commit 010ecf4
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 8 deletions.
12 changes: 5 additions & 7 deletions .github/workflows/library_rust_tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ jobs:
- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
dafny-version: 4.9.0
dafny-version: ${{ inputs.dafny }}

# TODO: Remove this after the formatting in Rust starts working
- name: smithy-dafny Rust hacks
Expand Down Expand Up @@ -133,22 +133,20 @@ jobs:
matrix:
library: [TestVectors]
os: [
windows-latest,
# Sed script doesn't work properly on windows
# windows-latest,
ubuntu-latest,
macos-13,
]
runs-on: ${{ matrix.os }}
permissions:
id-token: write
contents: read
env:
DOTNET_CLI_TELEMETRY_OPTOUT: 1
DOTNET_NOLOGO: 1
steps:
- name: Support longpaths on Git checkout
run: |
git config --global core.longpaths true
- uses: actions/checkout@v2
- uses: actions/checkout@v3
- name: Init Submodules
shell: bash
run: |
Expand All @@ -173,7 +171,7 @@ jobs:
- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
dafny-version: 4.9.0
dafny-version: ${{ inputs.dafny }}

# TODO: Remove this after the formatting in Rust starts working
- name: smithy-dafny Rust hacks
Expand Down
2 changes: 1 addition & 1 deletion TestVectors/dafny/TestVectors/test/RunMain.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ module {:extern} TestWrappedESDKMain {
)
);
print "ONLY WORRY IF THE ABOVE TESTS PASSED!!! THESE TESTS ARE SUPPOSED TO FAIL!\n";
print "IF THE TESTS FAIL OTHER THAN A AES GCM TAG VALIDATION EXCEPTION, CUT AN ISSUE.\n";
print "IF THE TESTS FAIL OTHER THAN A `AES GCM TAG VALIDATION EXCEPTION` or `AES Decrypt : gather Unspecified`, CUT AN ISSUE.\n";
print "IF THE TESTS ALL FAIL IT MEANS THE TEST PASSED!";
expect result.Failure?;
}
Expand Down

0 comments on commit 010ecf4

Please sign in to comment.