fix(ci): update CBMC proofs' Makefile.common

[tautschnig]

Description of changes:

In order to support upcoming work that uses loop invariants we need bugfixes to build rules, porting over what was already fixed upstream in model-checking/cbmc-starter-kit#195 (and further fixes starter kit's master branch).

Testing:

Tested in CI to make sure it does not adversely affect current CBMC proofs, and tested locally with upcoming work that will introduce loop invariants.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[rod-chapman]

I have re-generated all proofs with the change, and all is well. This is needed for moving forwards with unbounded proofs (i.e. getting rid of UNWINDSET).

[lrstewart]

This is marked ready for review, but the CBMC proofs are failing in CI.

[rod-chapman]

The CI runs gets to:

[2616/2689] s2n_stuffer_write_uint8: checking safety properties                 
Error: The operation was canceled.

Anyone know what that means?

[lrstewart]

The CI runs gets to:

[2616/2689] s2n_stuffer_write_uint8: checking safety properties                 
Error: The operation was canceled.

Anyone know what that means?

It says "Failing after 360m", so I'm guessing timeout?

Edit: definitely timeout. The summary for the job says "The job running on runner cbmc_ubuntu-latest_64-core_d5623345fda5 has exceeded the maximum execution time of 360 minutes."

[rod-chapman]

I am trying to reproduce this problem on an EC2 instance now.

[rod-chapman]

All proofs run fine on a 32-Core EC2 instance in about 7 minutes, so not sure what's wrong here.

[tautschnig]

This is marked ready for review, but the CBMC proofs are failing in CI.

This is now fixed, we had to retain malloc-may-fail for coverage checking.

[rod-chapman]

I have re-run all proofs on Intel/EC2 this morning on this branch, using both a wavefront build of CBMC, and release 6.1.0. All seems well. Can we get this merged now?

[tautschnig]

What to make of the S2nIntegrationV2SmallBatch failure?

[camshaft]

we've got a few flaky tests that need to be fixed. i just retried the failed job.