Superymk issues

Repositories
Issues
Comments

Results 2 issues of


                                            Superymk

Vale/Dafny does not generate invocation to the callee procedure if callee is defined after the caller function

Tested with Vale-0.3.10. Code: ``` procedure caller( out result:reg ) reads eax; modifies ebx; ecx; { callee(eax, ebx); MOV(ecx, ebx); } procedure callee( in bool1:reg, out result:reg ) reads eax;...

Any plan to release Vale with the latest Dafny?

Latest Dafny changes syntax a little bit. For example, Dafny-v1.9.9 complains "!new" which is needed in Dafny-v2.3 in my project. I also tried to build Vale with the latest Dafny...