fix: Remove reference to non-existent (in 1.x) commitment policy in new proof

robin-aws · robin-aws · commit 0fdaea526daa · 2021-05-05T09:28:20.000-07:00
diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/aws_cryptosdk_priv_algorithm_allowed_for_decrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/aws_cryptosdk_priv_algorithm_allowed_for_decrypt_harness.c
@@ -27,8 +27,7 @@ void aws_cryptosdk_priv_algorithm_allowed_for_decrypt_harness() {
 
     /* Function under test */
     int ret = aws_cryptosdk_priv_algorithm_allowed_for_decrypt(alg_id, policy);
-    if (policy == COMMITMENT_POLICY_FORBID_ENCRYPT_ALLOW_DECRYPT ||
-        policy == COMMITMENT_POLICY_REQUIRE_ENCRYPT_ALLOW_DECRYPT) {
+    if (policy == COMMITMENT_POLICY_FORBID_ENCRYPT_ALLOW_DECRYPT) {
         assert(ret == true);
     }
 

Original file line number	Diff line number	Diff line change
`@@ -27,8 +27,7 @@ void aws_cryptosdk_priv_algorithm_allowed_for_decrypt_harness() {`
`27`	`27`
`28`	`28`	`/* Function under test */`
`29`	`29`	`int ret = aws_cryptosdk_priv_algorithm_allowed_for_decrypt(alg_id, policy);`
`30`		`- if (policy == COMMITMENT_POLICY_FORBID_ENCRYPT_ALLOW_DECRYPT \|\|`
`31`		`- policy == COMMITMENT_POLICY_REQUIRE_ENCRYPT_ALLOW_DECRYPT) {`
	`30`	`+ if (policy == COMMITMENT_POLICY_FORBID_ENCRYPT_ALLOW_DECRYPT) {`
`32`	`31`	`assert(ret == true);`
`33`	`32`	`}`
`34`	`33`