Addresses one more review comment from MT.

Update harness example to use raw pointer actual parameters, not pointers to stack-allocated objects. Signed-off-by: Rod Chapman <[email protected]>
pq-code-package · Nov 6, 2024 · 6638384 · 6638384
1 parent 4a6e4e1
commit 6638384
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/cbmc/proofs/proof_guide.md b/cbmc/proofs/proof_guide.md
@@ -346,11 +346,11 @@ Note that `USE_FUNCTION_CONTRACTS` is left empty since `poly_tobytes()` is a lea
 
 ```
 void harness(void) {
-  poly a;
-  uint8_t r[MLKEM_POLYBYTES];
+  poly *a;
+  uint8_t *r;
 
   /* Contracts for this function are in poly.h */
-  poly_tobytes(r, &a);
+  poly_tobytes(r, a);
 }
 ```