From b2e7ca47449571beaca4a507c65ac3ee39d8eefc Mon Sep 17 00:00:00 2001
From: lucasmt <36549752+lucasmt@users.noreply.github.com>
Date: Tue, 9 Jul 2019 02:40:54 -0400
Subject: [PATCH] Add yaml file for aws_byte_buf_cat proof (#448)

* Proof harness for aws_byte_buf_cat with a fixed number of arguments
---
 .../jobs/aws_byte_buf_cat/aws_byte_buf_cat_harness.c       | 7 +------
 .cbmc-batch/jobs/aws_byte_buf_cat/cbmc-batch.yaml          | 4 ++++
 2 files changed, 5 insertions(+), 6 deletions(-)
 create mode 100644 .cbmc-batch/jobs/aws_byte_buf_cat/cbmc-batch.yaml

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
index a205fe860..c271f31b2 100644
--- 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
new file mode 100644
index 000000000..9985fd139
--- /dev/null
+++ 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"