vale

vale copied to clipboard

yizhou7

Create a fixed name for the while loop counter (loop_ctr)

1

yizhou7

Hello, I was wondering why the constant-time and leakage analysis code was removed in a previous [commit](https://github.com/project-everest/vale/commit/1ff348106874859ac8afab8b1d86ba4badda1be4) almost 2 years ago. Is there any specific reason behind this choice? Thanks...

ntauth

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;...

superymk


hz1490919302

Any plan to release Vale with the latest Dafny?

1

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...

superymk

How to count implementation lines written in Vale?

2

In Vale's paper, implementation lines which consist of assembly instructions and control-flow code are calculated. I've been building a system with Vale/Dafny and I am not sure how to calculate...

zpzigi

Currently, Vale/F* reports most verification errors in terms of the original Vale source code. However, the treatment of the "See also" reporting is current rather odd. In the example below,...

parno

Would it be reasonable for Vale to detect when you've included an entry in your reads or modifies clause that isn't actually needed? For example, if I include `rax` in...

parno

``` jonathan@genepi:~/Code/everest (master) $ mono vale/bin/vale.exe -h error processing file error: TODO: Implement command line help ```

msprotz