Add yaml file for aws_byte_buf_cat proof (awslabs#448)

* Proof harness for aws_byte_buf_cat with a fixed number of arguments
dougch · Jul 9, 2019 · b2e7ca4 · b2e7ca4
1 parent 22dd45d
commit b2e7ca4
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/.cbmc-batch/jobs/aws_byte_buf_cat/aws_byte_buf_cat_harness.c b/.cbmc-batch/jobs/aws_byte_buf_cat/aws_byte_buf_cat_harness.c
@@ -53,12 +53,7 @@ void aws_byte_buf_cat_harness() {
     save_byte_from_array(dest.buffer, dest.len, &old_byte_from_dest);
 
     /* operation under verification */
-    if (aws_byte_buf_cat(
-            nondet_bool() ? &dest : NULL,
-            number_of_args,
-            nondet_bool() ? &buffer1 : NULL,
-            nondet_bool() ? &buffer2 : NULL,
-            nondet_bool() ? &buffer3 : NULL) == AWS_OP_SUCCESS) {
+    if (aws_byte_buf_cat(&dest, number_of_args, &buffer1, &buffer2, &buffer3) == AWS_OP_SUCCESS) {
         assert((old_dest.capacity - old_dest.len) >= (buffer1.len + buffer2.len + buffer3.len));
     } else {
         assert((old_dest.capacity - old_dest.len) < (buffer1.len + buffer2.len + buffer3.len));

diff --git a/.cbmc-batch/jobs/aws_byte_buf_cat/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_byte_buf_cat/cbmc-batch.yaml
@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_byte_buf_cat.0:4;--object-bits;8"
+goto: aws_byte_buf_cat_harness.goto
+expected: "SUCCESSFUL"