Merge pull request #1039 from pq-code-package/cbmc_harness_fix

hanno-becker · web-flow · commit 97bfbfa49c42 · 2025-05-21T08:31:54.000+01:00
CBMC: Don't declare structures in harnesses
diff --git a/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c b/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c
@@ -9,6 +9,6 @@ void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);
 
 void harness(void)
 {
-  int16_t data[MLKEM_N];
+  int16_t *data;
   mlk_poly_permute_bitrev_to_custom(data);
 }
diff --git a/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c
@@ -7,7 +7,7 @@
 
 void harness(void)
 {
-  mlk_poly out[4];
-  uint8_t seed[4][MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
+  mlk_poly *out;
+  uint8_t(*seed)[MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
   mlk_poly_rej_uniform_x4(out, seed);
 }

Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,6 @@ void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);`
`9`	`9`
`10`	`10`	`void harness(void)`
`11`	`11`	`{`
`12`		`- int16_t data[MLKEM_N];`
	`12`	`+ int16_t *data;`
`13`	`13`	`mlk_poly_permute_bitrev_to_custom(data);`
`14`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@`
`7`	`7`
`8`	`8`	`void harness(void)`
`9`	`9`	`{`
`10`		`- mlk_poly out[4];`
`11`		`- uint8_t seed[4][MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];`
	`10`	`+ mlk_poly *out;`
	`11`	`+ uint8_t(*seed)[MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];`
`12`	`12`	`mlk_poly_rej_uniform_x4(out, seed);`
`13`	`13`	`}`