`static_attest` does nothing

[huynhtrankhanh]

This code snippet compiles when it is not supposed to. The static_attest(A[i] <= max_value); statement is used to tell the symbolic executor to verify that the max_value is indeed the biggest number in the array (it isn't) but ZZ doesn't reject the program as being invalid.

export fn main() -> int {
        usize n = 5;
        u64 A[n] = {3, 4, 5, 2, 1};
        u64 mut max_value = A[0];
/*
        for (usize mut i = 1; i < n; i++) {
                if (A[i] > max_value) {
                        max_value = A[i];
                }
        }
*/
        for (usize mut i = 0; i < n; i++) {
                static_attest(A[i] <= max_value);
        }
        return 0;
}

[huynhtrankhanh]

Oops, turns out static_attest does not do what I think it does. Sorry. But maybe you could document its usage somewhere.

[aep]

glad you figured it out, could you let me know what you thought it does?

[huynhtrankhanh]

I thought it would statically check the assertion I made using the SMT solver.

On Tue, Mar 10, 2020 at 5:08 PM Arvid E. Picciani notifications@github.com wrote:

glad you figured it out, could you let me know what you thought it does?

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/aep/zz/issues/29?email_source=notifications&email_token=AOW6J33UOGFC3SUUPQ5Z7CDRGYGRZA5CNFSM4LEYY4E2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEOKZBFQ#issuecomment-597004438, or unsubscribe https://github.com/notifications/unsubscribe-auth/AOW6J33NWRYYXNF35NHAJUDRGYGRZANCNFSM4LEYY4EQ .