diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index 7244fa87a..697cb875f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -132,7 +132,7 @@ module BeaconTestFixtures { kmsConfiguration := kmsConfig, logicalKeyStoreName := "KeyStoreDdbTable", grantTokens := None, - ddbTableName := "KeyStoreDdbTable", + ddbTableName := Some("KeyStoreDdbTable"), ddbClient := Some(ddbClient), kmsClient := Some(kmsClient) ); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy index 74e12264f..5dd0255ff 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy @@ -67,7 +67,7 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest { kmsConfiguration := kmsConfig, logicalKeyStoreName := logicalKeyStoreName, grantTokens := None, - ddbTableName := branchKeyStoreName, + ddbTableName := Some(branchKeyStoreName), ddbClient := Some(dynamodbClient), kmsClient := Some(kmsClient) ); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index 2667e361c..9d69f6a55 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -237,7 +237,7 @@ module TestFixtures { assume {:axiom} fresh(encryption.Modifies); } - method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option) + method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option) returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) ensures encryption.ValidState() ensures fresh(encryption) diff --git a/project.properties b/project.properties index 1a4050afc..1d808a93c 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ projectJavaVersion=3.6.2-SNAPSHOT -mplDependencyJavaVersion=1.5.1 +mplDependencyJavaVersion=1.5.1-SNAPSHOT dafnyVersion=4.2.0 dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0 diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index cdd4885cb..3801746b0 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d +Subproject commit 3801746b05a8154a512ffab88aa60d10993c9c79