From 7ffd47366bdc75faf59ee196ab85590e35eafd2d Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 4 Dec 2024 10:36:57 +0800 Subject: [PATCH] CBMC: Add missing function contract to shake128x4_absorb Signed-off-by: Matthias J. Kannwischer --- fips202/fips202x4.h | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/fips202/fips202x4.h b/fips202/fips202x4.h index e7bddacc5..59cb6aeb8 100644 --- a/fips202/fips202x4.h +++ b/fips202/fips202x4.h @@ -16,8 +16,15 @@ #define shake128x4_absorb FIPS202_NAMESPACE(shake128x4_absorb) void shake128x4_absorb(keccakx4_state *state, const uint8_t *in0, const uint8_t *in1, const uint8_t *in2, - const uint8_t *in3, size_t inlen); - + const uint8_t *in3, size_t inlen) +__contract__( + requires(memory_no_alias(state, sizeof(keccakx4_state))) + requires(memory_no_alias(in0, inlen)) + requires(memory_no_alias(in1, inlen)) + requires(memory_no_alias(in2, inlen)) + requires(memory_no_alias(in3, inlen)) + assigns(object_whole(state)) +); #define shake256x4_absorb FIPS202_NAMESPACE(shake256x4_absorb) void shake256x4_absorb(keccakx4_state *state, const uint8_t *in0,