From 52bbfeba8d82644350186f29ad173c839f64d3fe Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Tue, 8 Aug 2023 07:44:46 +0000 Subject: [PATCH] Update CBMC proof --- test/cbmc/proofs/CheckOptionsInner/Makefile.json | 4 ++-- test/cbmc/proofs/CheckOptionsOuter/Makefile.json | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index ada3510b2c..f318ae1cd4 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -2,8 +2,8 @@ "ENTRY": "CheckOptionsInner", "CBMCFLAGS": [ "--unwind 1", - "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.1:2", - "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.2:2" + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.1:2" ], "OPT": [ diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index 7220687090..d97be23e62 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json @@ -3,7 +3,7 @@ "CBMCFLAGS": [ "--unwind 1", - "--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.2:32" + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.0:32" ], "OPT": [