Skip to content

Commit

Permalink
Chore: Rust refactorings followup (#5793)
Browse files Browse the repository at this point in the history
Follow-up of #5786 with two
changes

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
MikaelMayer authored Sep 25, 2024
1 parent 8a4b1e7 commit cb91419
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 17 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ test-dafny:
echo "$$count test files found."; \
for file in $$files; do \
filedir=$$(dirname "$$file"); \
(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; "${DIR}"/Binaries/Dafny $(action) "$$(basename $$file)" ); \
(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; dotnet run --project "${DIR}"/Source/Dafny -- $(action) "$$(basename $$file)" ); \
done; \
fi

Expand Down
3 changes: 2 additions & 1 deletion Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -2201,7 +2201,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
case Eq(referential) => {
if (referential) {
if pointerType.Raw? {
r := Error("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)");
// Need to make comp/rust/traits.dfy to pass with --raw-pointer)
r := Error("Raw pointer comparison not properly implemented yet");
} else {
r := R.BinaryOp("==", left, right, DAST.Format.BinaryOpFormat.NoFormat());
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3215,7 +3215,7 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._
if (_14_referential) {
if (((this).pointerType).is_Raw) {
RAST._IExpr _out6;
_out6 = (this).Error(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)"), (this).InitEmptyExpr());
_out6 = (this).Error(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Raw pointer comparison not properly implemented yet"), (this).InitEmptyExpr());
r = _out6;
} else {
r = RAST.Expr.create_BinaryOp(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("=="), _8_left, _11_right, DAST.Format.BinaryOpFormat.create_NoFormat());
Expand Down
14 changes: 0 additions & 14 deletions Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit cb91419

Please sign in to comment.