Skip to content

Commit d6ea20b

Browse files
authored
feat: allow undersores in variable names (#383)
1 parent 1f44e54 commit d6ea20b

File tree

2 files changed

+6
-3
lines changed

2 files changed

+6
-3
lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -692,6 +692,8 @@ module DynamoDBFilterExpr {
692692
true
693693
else if '0' <= ch <= '9' then
694694
true
695+
else if ch == '_' then
696+
true
695697
else
696698
false
697699
}

DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ module TestDynamoDBFilterExpr {
3333
expect_equal(ParseExpr("and"), [And]);
3434
expect_equal(ParseExpr(" AnD "), [And]);
3535
expect_equal(ParseExpr(" A AnD B "), [MakeAttr("A"), And, MakeAttr("B")]);
36+
expect_equal(ParseExpr(" A_B AnD B_C "), [MakeAttr("A_B"), And, MakeAttr("B_C")]);
3637

3738
var input := [Not, MakeAttr("A"), In, Open, MakeAttr("B"), Comma, MakeAttr("C"), Close, Or];
3839
expect IsIN(input[1..]);
@@ -95,13 +96,13 @@ module TestDynamoDBFilterExpr {
9596
method {:test} TestBasicParse() {
9697
var context := ExprContext (
9798
None,
98-
Some("std2 = :A AND #Field4 = :B"),
99+
Some("std2 = :A AND #Field_4 = :B"),
99100
Some(map[
100101
":A" := DDB.AttributeValue.N("1.23"),
101102
":B" := DDB.AttributeValue.S("abc")
102103
]),
103104
Some(map[
104-
"#Field4" := "std4"
105+
"#Field_4" := "std4"
105106
])
106107
);
107108
var version := GetLotsaBeacons();
@@ -117,7 +118,7 @@ module TestDynamoDBFilterExpr {
117118

118119
var newContext :- expect BeaconizeParsedExpr(beaconVersion, parsed, 0, context.values.value, context.names, DontUseKeys, map[]);
119120
var exprString := ParsedExprToString(newContext.expr);
120-
expect exprString == "aws_dbe_b_std2 = :A AND #Field4 = :B";
121+
expect exprString == "aws_dbe_b_std2 = :A AND #Field_4 = :B";
121122
}
122123

123124
method {:test} TestNoBeaconFail() {

0 commit comments

Comments
 (0)