fix: Use the right >/</>=/<= comparison operators for bitvectors in JS #2716
Conversation
cpitclaudel
force-pushed
the
cpitclaudel_fix-2672
branch
4 times, most recently
from
a5ef771
to
d44dbe0
Compare
| // RUN: %dafny /compile:0 "%s" > "%t" | ||
| // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" | ||
| // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" | ||
| // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" | ||
| // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" | ||
| // RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t" | ||
| // RUN: %diff "%s.expect" "%t" |
There was a problem hiding this comment.
Can you use %testDafnyForEachCompiler %s instead? :)
There was a problem hiding this comment.
Can you remind me how to generate the output with that flag?
There was a problem hiding this comment.
It should just be a single copy of the program's output, not including the "Dafny program verifier ..." line. So in this case just:
true true true true true true true true true
false false false false false false false false false
false false false false false false false false false
true true true true true true true true true
true true true true true true true true true
false false false false false false false false false
true true true
false false false
It occurs to me that having a flag on the TestDafny tool to generate the expect file would be super handy, let me know see if I can add that. :)
There was a problem hiding this comment.
Thanks! Unfortunately it doesn't correctly detect unsupported features, so it fails on this example; I've reported the error at #2718 , and I'm currently preparing a PR. We can update this test file once that PR is merged, but I don't think we need to block on it.
There was a problem hiding this comment.
I'm not sure we should add the output generation to TestDafny, btw, since it's needed for all lit tests (not just for for-each-compiler). Maybe we could update runTest.py to recognize that case in addition to the usual diff-based ones.
There was a problem hiding this comment.
I think both makes sense. Since LIT tests can be more complicated than just piping to a single *.expect file, runTest.py can't realistically generate the "expected output" for an arbitrary LIT test (nor would this make sense as a feature on the xUnit-based LIT test runner either). I say we update it to recognize %testDafnyForEachCompiler but have it delegate generating the output file to TestDafny.
Part of the reason I'd prefer that is I'd also find it useful to install testdafny as a local dotnet tool and run it in this mode on arbitrary source files as part of development.
| callString = "isLessThan"; | ||
| } else { | ||
| opString = "<"; | ||
| Contract.Assert(false); |
There was a problem hiding this comment.
AFAICT we always throw new cce.UnreachableException(); after such a contract assertion. That ensures control flow doesn't just continue in release builds.
cpitclaudel
force-pushed
the
cpitclaudel_fix-2672
branch
from
d44dbe0
to
45d3a1a
Compare
cpitclaudel
force-pushed
the
cpitclaudel_fix-2672
branch
from
45d3a1a
to
447f888
Compare
Closes #2672.