diff options
Diffstat (limited to 'src/noise.c')
| -rw-r--r-- | src/noise.c | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/noise.c b/src/noise.c index 890b5b5..949a68d 100644 --- a/src/noise.c +++ b/src/noise.c @@ -199,8 +199,6 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); - assigns key_checked_trace; - ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; ensures (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==> key_match_trace == 1 || (st->failed_handshakes > \old(st->failed_handshakes)); |