From 447d084d79cc139d0aaa4433148cc7c310bfaf0d Mon Sep 17 00:00:00 2001
From: jaseg <git@jaseg.net>
Date: Mon, 17 Dec 2018 13:38:39 +0900
Subject: First steps to prove cobs decoder

---
 src/noise.c | 2 --
 1 file changed, 2 deletions(-)

(limited to 'src/noise.c')

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));
-- 
cgit