From 8b0b1f031e079a2501aab630cb7a00695b0204d8 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 2 Aug 2024 10:08:09 +0000 Subject: [PATCH] Add one more stub function to satisfy CBMC 6.1 on EC2/Linux Signed-off-by: Ubuntu --- tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile | 1 + tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile | 1 + tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile | 1 + tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile | 1 + 4 files changed, 4 insertions(+) diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile index c672aef27f6..de878adf70e 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile @@ -28,6 +28,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c PROOF_SOURCES += $(PROOF_STUB)/mlock.c PROOF_SOURCES += $(PROOF_STUB)/munlock.c +PROOF_SOURCES += $(PROOF_STUB)/madvise.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile index f3c18adceee..c6c8c1d3974 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile @@ -28,6 +28,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c PROOF_SOURCES += $(PROOF_STUB)/mlock.c PROOF_SOURCES += $(PROOF_STUB)/munlock.c +PROOF_SOURCES += $(PROOF_STUB)/madvise.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile index 87273e2eed0..0fd96bd3162 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile @@ -25,6 +25,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c PROOF_SOURCES += $(PROOF_STUB)/mlock.c PROOF_SOURCES += $(PROOF_STUB)/munlock.c +PROOF_SOURCES += $(PROOF_STUB)/madvise.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile index ff2727ffd7c..b943356821f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile @@ -25,6 +25,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c PROOF_SOURCES += $(PROOF_STUB)/mlock.c PROOF_SOURCES += $(PROOF_STUB)/munlock.c +PROOF_SOURCES += $(PROOF_STUB)/madvise.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c