Skip to content

Commit 3a10d92

Browse files
tautschnigtautschnig
committed
Adjust proof tooling to support CBMC v6
With CBMC v6, unwinding assertions are enabled by default, and object bits no longer need to be set at compile time. Update various build rules to use the latest template as provided with CBMC starter kit. Also fixes missing function definitions.
1 parent a5cd1c0 commit 3a10d92

File tree

33 files changed

+493
-213
lines changed

33 files changed

+493
-213
lines changed

‎.github/workflows/ci.yml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,7 @@ jobs:
261261
- name: Set up CBMC runner
262262
uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
263263
with:
264-
cbmc_version: "5.61.0"
265-
cbmc_viewer_version: "3.5"
264+
cbmc_version: "6.3.1"
266265
- name: Install cmake
267266
run: |
268267
sudo apt-get install -y cmake

‎source/core_pkcs11.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@
3030
/* C runtime includes. */
3131
#include <stdio.h>
3232
#include <stdint.h>
33+
#include <stdlib.h>
3334
#include <string.h>
3435

3536
/**

‎test/cbmc/proofs/C_CloseSession/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_CloseSession_harness
99
PROOF_UID = C_CloseSession
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY += C_Finalize
1616
REMOVE_FUNCTION_BODY += C_GetFunctionList

‎test/cbmc/proofs/C_CreateObject/Makefile

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,14 @@ MAX_LABEL_SIZE=32
2525
# Should be one more than the total number of objects in the PKCS stack.
2626
MAX_OBJECT_NUM=2
2727

28+
CBMC_OBJECT_BITS = 9
29+
2830
DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE)
2931
DEFINES += -DTEMPLATE_ATTRIBUTE_MAX_SIZE=$(TEMPLATE_ATTRIBUTE_MAX_SIZE)
3032

31-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
3233
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
34+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
35+
INCLUDES += -I$(SRCDIR)/source/portable/os
3336

3437
REMOVE_FUNCTION_BODY += C_Initialize
3538
REMOVE_FUNCTION_BODY += C_Finalize
@@ -61,5 +64,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
6164
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
6265
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
6366
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
67+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
6468

6569
include ../Makefile.common

‎test/cbmc/proofs/C_DestroyObject/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ MAX_LABEL_SIZE=32
1616

1717
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
1818

19-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
2019
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
20+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
2121

2222
REMOVE_FUNCTION_BODY += C_Finalize
2323
REMOVE_FUNCTION_BODY += C_GetFunctionList

‎test/cbmc/proofs/C_DigestFinal/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestFinal_harness
99
PROOF_UID = C_DigestFinal
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_DigestInit/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestInit_harness
99
PROOF_UID = C_DigestInit
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_DigestUpdate/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestUpdate_harness
99
PROOF_UID = C_DigestUpdate
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_Finalize/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_Finalize_harness
99
PROOF_UID = C_Finalize
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_FindObjects/Makefile

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,20 +9,24 @@ HARNESS_FILE = C_FindObjects_harness
99
PROOF_UID = C_FindObjects
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
14+
INCLUDES += -I$(SRCDIR)/source/portable/os
1415

1516
REMOVE_FUNCTION_BODY += C_Finalize
1617
REMOVE_FUNCTION_BODY += C_GetFunctionList
1718

1819
# This should be similar to the dummy data length in "core_pkcs11_pal_stubs.c" PKCS11_PAL_GetObjectValue
1920
UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvFindObjectInListByLabel.0:13
21+
UNWINDSET += strncmp.0:20
2022
# This should align with the max object count configured in core_pkcs11_config.h
2123
UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvAddObjectToList.0:2
2224

2325
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2426
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
2527
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
2628
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
29+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
30+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/core_pkcs11_pal_utils.c
2731

2832
include ../Makefile.common

‎test/cbmc/proofs/C_FindObjectsFinal/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_FindObjectsFinal_harness
99
PROOF_UID = C_FindObjectsFinal
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_FindObjectsInit/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ PROOF_UID = C_FindObjectsInit
1111
TEMPLATE_SIZE=10
1212

1313
DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE)
14-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1514
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
15+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1616

1717
REMOVE_FUNCTION_BODY +=
1818
UNWINDSET += C_FindObjectsInit.0:$(TEMPLATE_SIZE)

‎test/cbmc/proofs/C_GenerateKeyPair/Makefile

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ TEMPLATE_SIZE=10
1212

1313
DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE)
1414

15-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1615
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
16+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
17+
INCLUDES += -I$(SRCDIR)/source/portable/os
1718

1819
REMOVE_FUNCTION_BODY += C_Initialize
1920
REMOVE_FUNCTION_BODY += C_Finalize
@@ -29,6 +30,7 @@ UNWINDSET += harness.0:10
2930
UNWINDSET += harness.1:10
3031
UNWINDSET += memcmp.0:32
3132
UNWINDSET += memcpy.0:32
33+
UNWINDSET += strncmp.0:20
3234

3335
# The nested memcmp in this loop will exponentially increase the CBMC bounds checking.
3436
# Be very careful increasing this. At the time of writing this, the PKCS stack was
@@ -42,5 +44,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4244
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
4345
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
4446
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
47+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
48+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/core_pkcs11_pal_utils.c
4549

4650
include ../Makefile.common

‎test/cbmc/proofs/C_GenerateRandom/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_GenerateRandom_harness
99
PROOF_UID = C_GenerateRandom
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY += C_Initialize
1616
REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvMbedTLS_Initialize

‎test/cbmc/proofs/C_GetAttributeValue/Makefile

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,9 @@ MAX_OBJECT_NUM=2
2020

2121
DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE)
2222
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
23-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
2423
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
24+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
25+
INCLUDES += -I$(SRCDIR)/source/portable/os
2526

2627
REMOVE_FUNCTION_BODY +=
2728

@@ -37,5 +38,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3738
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
3839
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
3940
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
41+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
4042

4143
include ../Makefile.common

‎test/cbmc/proofs/C_GetFunctionList/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_GetFunctionList_harness
99
PROOF_UID = C_GetFunctionList
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

‎test/cbmc/proofs/C_GetMechanismInfo/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_GetMechanismInfo_harness
99
PROOF_UID = C_GetMechanismInfo
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616

‎test/cbmc/proofs/C_GetSlotList/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_GetSlotList_harness
99
PROOF_UID = C_GetSlotList
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
# This proof doesn't care about these stubs
1616
REMOVE_FUNCTION_BODY += C_Finalize

‎test/cbmc/proofs/C_Initialize/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_Initialize_harness
99
PROOF_UID = C_Initialize
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY += C_Finalize
1616
REMOVE_FUNCTION_BODY += C_GetFunctionList

‎test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ void harness()
3737
CK_SESSION_HANDLE * pxSession = malloc( sizeof( CK_SESSION_HANDLE ) );
3838

3939
xResult = C_Initialize( NULL );
40-
__CPROVER__assume( xResult == CKR_OK );
40+
__CPROVER_assume( xResult == CKR_OK );
4141

4242
xResult = C_OpenSession( 0, xFlags, NULL, 0, pxSession );
4343

‎test/cbmc/proofs/C_OpenSession/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_OpenSession_harness
99
PROOF_UID = C_OpenSession
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1414

1515
REMOVE_FUNCTION_BODY += C_Finalize
1616
REMOVE_FUNCTION_BODY += C_GetFunctionList

‎test/cbmc/proofs/C_Sign/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ PROOF_UID = C_Sign
1313
MAX_OBJECT_NUM=2
1414

1515
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
16-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1716
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
17+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1818

1919
REMOVE_FUNCTION_BODY += C_Initialize
2020
REMOVE_FUNCTION_BODY += C_OpenSession

‎test/cbmc/proofs/C_SignInit/Makefile

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ PROOF_UID = C_SignInit
1313
MAX_OBJECT_NUM=2
1414

1515
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
16-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1716
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
17+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
18+
INCLUDES += -I$(SRCDIR)/source/portable/os
1819

1920
REMOVE_FUNCTION_BODY += C_Initialize
2021
REMOVE_FUNCTION_BODY += C_OpenSession
@@ -32,5 +33,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3233
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
3334
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
3435
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
36+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
3537

3638
include ../Makefile.common

‎test/cbmc/proofs/C_Verify/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ PROOF_UID = C_Verify
1313
MAX_OBJECT_NUM=2
1414

1515
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
16-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1716
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
17+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
1818

1919
REMOVE_FUNCTION_BODY += C_Initialize
2020
REMOVE_FUNCTION_BODY += C_OpenSession

‎test/cbmc/proofs/C_VerifyInit/Makefile

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ PROOF_UID = C_VerifyInit
1313
MAX_OBJECT_NUM=2
1414

1515
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
16-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1716
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
17+
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls/include
18+
INCLUDES += -I$(SRCDIR)/source/portable/os
1819

1920
REMOVE_FUNCTION_BODY += C_Initialize
2021
REMOVE_FUNCTION_BODY += C_OpenSession
@@ -34,5 +35,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3435
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
3536
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
3637
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
38+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
3739

3840
include ../Makefile.common

‎test/cbmc/proofs/Makefile-project-targets

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,13 @@
88
# Use this file to give project-specific targets, including targets
99
# that may depend on targets defined in Makefile.common.
1010
################################################################
11+
12+
$(PROJECT_SOURCES): $(SRCDIR)/test/build/_deps/mbedtls_2-src/include/mbedtls/pk.h
13+
14+
$(SRCDIR)/test/build/_deps/mbedtls_2-src/include/mbedtls/pk.h:
15+
if [ ! -f $@ ] ; then cd $(SRCDIR)/test && cmake -B build ; fi
16+
17+
clean: clean_mbedtls
18+
19+
clean_mbedtls:
20+
$(RM) -r $(SRCDIR)/test/build

0 commit comments

Comments
 (0)