Skip to content

Commit eb65541

Browse files
Add extern
1 parent d988c6e commit eb65541

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

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

35+
const {:extern "Utils.constants", "getDefaultKeys"} DEFAULT_KEYS : string
3536

3637
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
3738
type ConfigName = string
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package filepath;
2+
3+
public class Constants {
4+
public static dafny.DafnySequence<? extends Character> defaultKeys(){
5+
return dafny.DafnySequence.asString("../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json");
6+
}
7+
}

0 commit comments

Comments
 (0)