CBMC Batch scripts seem to need buckets and packages specified

[cmangla]

I built the latest aws-batch-cbmc, deployed on a new AWS account, and ran the aws-c-common CBMC tests. I needed to modify cbmc-batch.sh to get the tests to work correctly.

At

aws-c-common/.cbmc-batch/cbmc-batch.sh

Line 25 in 40296d9

cbmc-batch \

I had to add the following flags:

--srcbucket s3://.../cbmc/srcbucket \
--wsbucket s3://.../cbmc/wsbucket/$job \
--outbucket s3://.../cbmc/outbucket/$job \
--pkgbucket s3://.../cbmc/package \
--cbmcpkg cbmc-ubuntu16.tar.gz \
--batchpkg cbmc-batch.tar.gz \
--viewerpkg cbmc-viewer.tar.gz \

The outbucket needed the $job subdirectory, without which the different tests were overwriting each other's files (I think).

Steps to reproduce:

1. Build and deploy aws-batch-cbmc
2. Set $PATH to cbmc-batch of aws-batch-cbmc.
3. Clone aws-c-common and run cbmc-batch.sh --start in .cbmc-batch/.
4. Notice complains about missing *bucket specification.
5. Add the above flags but without the $job subdirectory.
6. Run cbmc-batch.sh and see tests failing and getting utterly confused.
7. Add the $job subdirectories as shown above and see the jobs all pass.

[jmklix]

Thanks for opening this, but we don't use this script anymore. Closing this issue