Skip to content

Commit

Permalink
Add missing stubs to satisfy CBMC 6.1 for these proofs
Browse files Browse the repository at this point in the history
Signed-off-by: Rod Chapman <rodchap@amazon.com>
  • Loading branch information
rod-chapman committed Aug 2, 2024
1 parent edfa9f7 commit 850d50c
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 0 deletions.
2 changes: 2 additions & 0 deletions tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
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

PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
Expand Down
2 changes: 2 additions & 0 deletions tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
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

PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
Expand Down
2 changes: 2 additions & 0 deletions tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
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

PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
Expand Down
2 changes: 2 additions & 0 deletions tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
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

PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
Expand Down

0 comments on commit 850d50c

Please sign in to comment.