Skip to content

Commit eeee4b3

Browse files
Add ReturnValues
1 parent b8c918e commit eeee4b3

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -901,7 +901,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
901901
Key := map[HashName := records[i].item[HashName]],
902902
ConditionExpression := Some(conditionExpr),
903903
ExpressionAttributeNames := Some(exprAttrNames),
904-
ExpressionAttributeValues := Some(exprAttrValues)
904+
ExpressionAttributeValues := Some(exprAttrValues),
905+
ReturnValues := Some(DDB.ReturnValue.ALL_OLD)
905906
);
906907

907908
// The delete operation will succeed only if the condition is met
@@ -918,9 +919,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
918919
expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException";
919920
} else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == valueToDelete {
920921
expect deleteResult.Success?;
922+
print("\n");
923+
print(deleteResult);
921924
} else {
922925
expect deleteResult.Failure?, "DeleteItem should have failed.";
923-
expect deleteResult.error.ConditionalCheckFailedException?;
926+
expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException";
924927
}
925928
}
926929
}

0 commit comments

Comments
 (0)