Rename CBMC proof bound BLOB_SIZE -> MAX_BLOB_SIZE (#3073)

Co-authored-by: Mark R. Tuttle <[email protected]>
aws · Oct 5, 2021 · 270bfbb · 270bfbb
1 parent 4513f8d
commit 270bfbb
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 12 deletions.
diff --git a/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile b/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile
@@ -13,8 +13,8 @@
 
 
 # Enough to get full coverage with 10 seconds of runtime.
-BLOB_SIZE = 10
-DEFINES += -DBLOB_SIZE=$(BLOB_SIZE)
+MAX_BLOB_SIZE = 10
+DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE)
 
 CBMCFLAGS +=
 
@@ -34,6 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 # We abstract this function because manual inspection demonstrates it is unreachable.
 REMOVE_FUNCTION_BODY += s2n_calculate_stacktrace
 
-UNWINDSET += s2n_blob_char_to_lower.1:$(call addone,$(BLOB_SIZE))
+UNWINDSET += s2n_blob_char_to_lower.1:$(call addone,$(MAX_BLOB_SIZE))
 
 include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_blob_char_to_lower/s2n_blob_char_to_lower_harness.c b/tests/cbmc/proofs/s2n_blob_char_to_lower/s2n_blob_char_to_lower_harness.c
@@ -25,7 +25,7 @@ void s2n_blob_char_to_lower_harness()
     /* Non-deterministic inputs. */
     struct s2n_blob *blob = cbmc_allocate_s2n_blob();
     __CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(blob)));
-    __CPROVER_assume(s2n_blob_is_bounded(blob, BLOB_SIZE));
+    __CPROVER_assume(s2n_blob_is_bounded(blob, MAX_BLOB_SIZE));
 
     /* Save previous state. */
     struct s2n_blob               old_blob = *blob;

diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile
@@ -12,8 +12,8 @@
 # limitations under the License.
 
 # Enough to get full coverage with 10 seconds of runtime.
-BLOB_SIZE = 10
-DEFINES += -DBLOB_SIZE=$(BLOB_SIZE)
+MAX_BLOB_SIZE = 10
+DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE)
 
 CBMCFLAGS +=
 
@@ -30,6 +30,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 
-UNWINDSET += s2n_stuffer_skip_expected_char.4:$(call addone,$(BLOB_SIZE))
+UNWINDSET += s2n_stuffer_skip_expected_char.4:$(call addone,$(MAX_BLOB_SIZE))
 
 include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/s2n_stuffer_skip_expected_char_harness.c b/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/s2n_stuffer_skip_expected_char_harness.c
@@ -25,7 +25,7 @@ void s2n_stuffer_skip_expected_char_harness()
     /* Non-deterministic inputs. */
     struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer();
     __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer)));
-    __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, BLOB_SIZE));
+    __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, MAX_BLOB_SIZE));
     const char expected;
     uint32_t   min;
     uint32_t   max;

diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile
@@ -12,8 +12,8 @@
 # limitations under the License.
 
 # Enough to get full coverage with 40 seconds of runtime.
-BLOB_SIZE = 10
-DEFINES += -DBLOB_SIZE=$(BLOB_SIZE)
+MAX_BLOB_SIZE = 10
+DEFINES += -DMAX_BLOB_SIZE=$(MAX_BLOB_SIZE)
 
 PROOF_UID = s2n_stuffer_skip_to_char
 HARNESS_ENTRY = $(PROOF_UID)_harness
@@ -30,6 +30,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 
-UNWINDSET += s2n_stuffer_skip_to_char.1:$(call addone,$(BLOB_SIZE))
+UNWINDSET += s2n_stuffer_skip_to_char.1:$(call addone,$(MAX_BLOB_SIZE))
 
 include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_to_char/s2n_stuffer_skip_to_char_harness.c b/tests/cbmc/proofs/s2n_stuffer_skip_to_char/s2n_stuffer_skip_to_char_harness.c
@@ -26,7 +26,7 @@ void s2n_stuffer_skip_to_char_harness()
     /* Non-deterministic inputs. */
     struct s2n_stuffer *stuffer = cbmc_allocate_s2n_stuffer();
     __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(stuffer)));
-    __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, BLOB_SIZE));
+    __CPROVER_assume(s2n_blob_is_bounded(&stuffer->blob, MAX_BLOB_SIZE));
     const char target;
 
     /* Save previous state from stuffer. */