chore: Bring TcpRepr specifics into proofs

smoltcp-rs · Sep 29, 2023 · a440600 · a440600
1 parent 1cb548a
commit a440600
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/socket/tcp.rs b/src/socket/tcp.rs
@@ -7905,6 +7905,7 @@ mod verification {
                 && p.control == TcpControl::Syn
                 && p.ack_number == None
                 && p.seq_number == remote_seq
+                && p.max_seg_size != Some(0)
                 && p.window_scale == window_scale
         });
 
@@ -7936,6 +7937,7 @@ mod verification {
                 && p.control == TcpControl::None
                 && p.ack_number == Some(local_seq + 1)
                 && p.seq_number == remote_seq + 1
+                && p.max_seg_size != Some(0)
                 && p.window_scale == None
         });