Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,11 @@ module DdbMiddlewareConfig {
function SearchModifies(config: Config) : set<object>
{
//set x, y | y in config.tableEncryptionConfigs && x in OneSearchModifies(config.tableEncryptionConfigs[y]) :: x
set versions <- set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions,
keyStore <- set version <- versions :: version.keySource.store,
obj <- keyStore.Modifies | obj in keyStore.Modifies :: obj
set
versions <- (set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions),
keyStore <- (set version <- versions :: version.keySource.store),
obj <- keyStore.Modifies
{:nowarn} :: obj

}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ module
+ (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
+ (if tableConfig.search.Some? then tableConfig.search.value.versions[0].keyStore.Modifies else {})
)
:: o;
{:nowarn} :: o; // ignore warning for missing trigger on quantifier

var allLogicalTableNames := {};
var i := 0;
Expand Down
6 changes: 3 additions & 3 deletions SharedMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk

VERIFY_TIMEOUT := 250

verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv

transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts
Expand Down
Loading