Skip to content

Commit 223a413

Browse files
Add extern
1 parent eb65541 commit 223a413

File tree

2 files changed

+7
-2
lines changed

2 files changed

+7
-2
lines changed

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
3232
import CreateInterceptedDDBClient
3333
import DynamoDbItemEncryptor
3434

35-
const {:extern "Utils.constants", "getDefaultKeys"} DEFAULT_KEYS : string
36-
3735
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
3836
type ConfigName = string
3937

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package Utils;
2+
3+
public class constants {
4+
public static dafny.DafnySequence<? extends Character> getDefaultKeys(){
5+
return dafny.DafnySequence.asString("../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json");
6+
}
7+
}

0 commit comments

Comments
 (0)