diff --git a/src/expression.md b/src/expression.md index 2c031a5..6745ad5 100644 --- a/src/expression.md +++ b/src/expression.md @@ -89,8 +89,6 @@ module SOLIDITY-EXPRESSION ... X |-> var(_ => I, T) ... // assignment to array element - context HOLE [ _ ] = _ - context _ [ HOLE ] = _ rule lv(I:Int, L, LT []) [ Idx:Int ] = v(V, RT) => v(convert(V, RT, LT), LT) ... S => S [ I <- write({S [ I ]}:>Value, L ListItem(Idx), convert(V, RT, LT), LT[]) ] rule lv(I:Int, L, LT []) [ v(Idx:MInt{256}, _) ] = v(V, RT) => v(convert(V, RT, LT), LT) ... @@ -109,8 +107,6 @@ module SOLIDITY-EXPRESSION rule write(M:Map, ListItem(Key:Value) L2, V, mapping(_ _ => T2)) => M [ Key <- write({M [ Key ] orDefault default(T2)}:>Value, L2, V, T2) ] // type conversion - context _:ElementaryTypeName ( HOLE:CallArgumentList ) - context _:Id ( HOLE:CallArgumentList ) rule uint32(v(V:MInt{256}, _)) => v(roundMInt(V)::MInt{32}, uint32) rule uint112(v(V:MInt{256}, _)) => v(roundMInt(V)::MInt{112}, uint112) rule uint256(v(V:MInt{112}, _)) => v(roundMInt(V)::MInt{256}, uint256) @@ -149,8 +145,6 @@ module SOLIDITY-EXPRESSION requires isAggregateType(T) // array element lookup - context HOLE:Expression [ _:Expression ] - context _:Expression [ HOLE:Expression ] rule lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ... _ [ I <- V ] requires notBool isAggregateType(T) @@ -180,13 +174,10 @@ module SOLIDITY-EXPRESSION // array length syntax Id ::= "length" [token] - context HOLE . length rule lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ... _ [ I <- V ] // external call - context HOLE . _ ( _:CallArgumentList ) - context (_ . _) ( HOLE:CallArgumentList ) rule v(ADDR, _) . F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); FROM => THIS VALUE => 0p256 @@ -209,10 +200,6 @@ module SOLIDITY-EXPRESSION syntax Id ::= "value" [token] - context HOLE . _ { value: _ } ( _ ) - context _ . _ { value: HOLE } ( _ ) - context _ . _ { _ } ( HOLE:CallArgumentList ) - rule v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); FROM => THIS VALUE => VALUE' @@ -515,4 +502,167 @@ module SOLIDITY-EXPRESSION rule retval(.List) => void rule retval(ListItem(noId)) => void rule retval(ListItem(X:Id)) => X + + // Heating and cooling rules + syntax KItem ::= freezerAssignment(Expression) + rule E:Expression = HOLE:Expression => HOLE ~> freezerAssignment(E) ... [heat] + rule HOLE:Expression ~> freezerAssignment(E) => E = HOLE ... [cool] + + syntax KItem ::= freezerTernaryOperator(Expression, Expression) + rule HOLE:Expression ? E1:Expression : E2:Expression => HOLE ~> freezerTernaryOperator(E1, E2) ... [heat] + rule HOLE:Expression ~> freezerTernaryOperator(E1, E2) => HOLE ? E1 : E2 ... [cool] + + syntax KItem ::= freezerOr(Expression) + rule HOLE:Expression || E:Expression => HOLE ~> freezerOr(E) ... [heat] + rule HOLE:Expression ~> freezerOr(E) => HOLE || E ... [cool] + + syntax KItem ::= freezerAnd(Expression) + rule HOLE:Expression && E:Expression => HOLE ~> freezerAnd(E) ... [heat] + rule HOLE:Expression ~> freezerAnd(E) => HOLE && E ... [cool] + + syntax KItem ::= freezerEq1(Expression) + | freezerEq2(Expression) + rule HOLE:Expression == E:Expression => HOLE ~> freezerEq1(E) ... [heat] + rule HOLE:Expression ~> freezerEq1(E) => HOLE == E ... [cool] + rule E:Expression == HOLE:Expression => HOLE ~> freezerEq2(E) ... [heat] + rule HOLE:Expression ~> freezerEq2(E) => E == HOLE ... [cool] + + syntax KItem ::= freezerNeq1(Expression) + | freezerNeq2(Expression) + rule HOLE:Expression != E:Expression => HOLE ~> freezerNeq1(E) ... [heat] + rule HOLE:Expression ~> freezerNeq1(E) => HOLE != E ... [cool] + rule E:Expression != HOLE:Expression => HOLE ~> freezerNeq2(E) ... [heat] + rule HOLE:Expression ~> freezerNeq2(E) => E != HOLE ... [cool] + + syntax KItem ::= freezerLt1(Expression) + | freezerLt2(Expression) + rule HOLE:Expression < E:Expression => HOLE ~> freezerLt1(E) ... [heat] + rule HOLE:Expression ~> freezerLt1(E) => HOLE < E ... [cool] + rule E:Expression < HOLE:Expression => HOLE ~> freezerLt2(E) ... [heat] + rule HOLE:Expression ~> freezerLt2(E) => E < HOLE ... [cool] + + syntax KItem ::= freezerLeq1(Expression) + | freezerLeq2(Expression) + rule HOLE:Expression <= E:Expression => HOLE ~> freezerLeq1(E) ... [heat] + rule HOLE:Expression ~> freezerLeq1(E) => HOLE <= E ... [cool] + rule E:Expression <= HOLE:Expression => HOLE ~> freezerLeq2(E) ... [heat] + rule HOLE:Expression ~> freezerLeq2(E) => E <= HOLE ... [cool] + + syntax KItem ::= freezerGt1(Expression) + | freezerGt2(Expression) + rule HOLE:Expression > E:Expression => HOLE ~> freezerGt1(E) ... [heat] + rule HOLE:Expression ~> freezerGt1(E) => HOLE > E ... [cool] + rule E:Expression > HOLE:Expression => HOLE ~> freezerGt2(E) ... [heat] + rule HOLE:Expression ~> freezerGt2(E) => E > HOLE ... [cool] + + syntax KItem ::= freezerGeq1(Expression) + | freezerGeq2(Expression) + rule HOLE:Expression >= E:Expression => HOLE ~> freezerGeq1(E) ... [heat] + rule HOLE:Expression ~> freezerGeq1(E) => HOLE >= E ... [cool] + rule E:Expression >= HOLE:Expression => HOLE ~> freezerGeq2(E) ... [heat] + rule HOLE:Expression ~> freezerGeq2(E) => E >= HOLE ... [cool] + + syntax KItem ::= freezerAdd1(Expression) + | freezerAdd2(Expression) + rule HOLE:Expression + E:Expression => HOLE ~> freezerAdd1(E) ... [heat] + rule HOLE:Expression ~> freezerAdd1(E) => HOLE + E ... [cool] + rule E:Expression + HOLE:Expression => HOLE ~> freezerAdd2(E) ... [heat] + rule HOLE:Expression ~> freezerAdd2(E) => E + HOLE ... [cool] + + syntax KItem ::= freezerSub1(Expression) + | freezerSub2(Expression) + rule HOLE:Expression - E:Expression => HOLE ~> freezerSub1(E) ... [heat] + rule HOLE:Expression ~> freezerSub1(E) => HOLE - E ... [cool] + rule E:Expression - HOLE:Expression => HOLE ~> freezerSub2(E) ... [heat] + rule HOLE:Expression ~> freezerSub2(E) => E - HOLE ... [cool] + + syntax KItem ::= freezerMul1(Expression) + | freezerMul2(Expression) + rule HOLE:Expression * E:Expression => HOLE ~> freezerMul1(E) ... [heat] + rule HOLE:Expression ~> freezerMul1(E) => HOLE * E ... [cool] + rule E:Expression * HOLE:Expression => HOLE ~> freezerMul2(E) ... [heat] + rule HOLE:Expression ~> freezerMul2(E) => E * HOLE ... [cool] + + syntax KItem ::= freezerDiv1(Expression) + | freezerDiv2(Expression) + rule HOLE:Expression / E:Expression => HOLE ~> freezerDiv1(E) ... [heat] + rule HOLE:Expression ~> freezerDiv1(E) => HOLE / E ... [cool] + rule E:Expression / HOLE:Expression => HOLE ~> freezerDiv2(E) ... [heat] + rule HOLE:Expression ~> freezerDiv2(E) => E / HOLE ... [cool] + + syntax KItem ::= freezerMod1(Expression) + | freezerMod2(Expression) + rule HOLE:Expression % E:Expression => HOLE ~> freezerMod1(E) ... [heat] + rule HOLE:Expression ~> freezerMod1(E) => HOLE % E ... [cool] + rule E:Expression % HOLE:Expression => HOLE ~> freezerMod2(E) ... [heat] + rule HOLE:Expression ~> freezerMod2(E) => E % HOLE ... [cool] + + syntax KItem ::= freezerExp1(Expression) + | freezerExp2(Expression) + rule HOLE:Expression ** E:Expression => HOLE ~> freezerExp1(E) ... [heat] + rule HOLE:Expression ~> freezerExp1(E) => HOLE ** E ... [cool] + rule E:Expression ** HOLE:Expression => HOLE ~> freezerExp2(E) ... [heat] + rule HOLE:Expression ~> freezerExp2(E) => E ** HOLE ... [cool] + + syntax KItem ::= freezerNew(TypeName) + rule new T:TypeName ( HOLE:CallArgumentList ) => HOLE ~> freezerNew(T) ... [heat] + rule HOLE:CallArgumentList ~> freezerNew(T) => new T ( HOLE ) ... [cool] + + syntax KItem ::= freezerCallArgumentListHead(Expression) + | freezerCallArgumentListTail(CallArgumentList) + rule HOLE:Expression, L:CallArgumentList => HOLE ~> freezerCallArgumentListTail(L) ... [heat] + rule HOLE:Expression ~> freezerCallArgumentListTail(L) => HOLE, L ... [cool] + rule E:Expression, HOLE:CallArgumentList => HOLE ~> freezerCallArgumentListHead(E) ... [heat] + rule HOLE:CallArgumentList ~> freezerCallArgumentListHead(E) => E, HOLE ... [cool] + + syntax KItem ::= freezerTypedValsHead(TypedVal) + | freezerTypedValsTail(TypedVals) + rule HOLE:TypedVal, L:TypedVals => HOLE ~> freezerTypedValsTail(L) ... [heat] + rule HOLE:TypedVal ~> freezerTypedValsTail(L) => HOLE, L ... [cool] + rule E:TypedVal, HOLE:TypedVals => HOLE ~> freezerTypedValsHead(E) ... [heat] + rule HOLE:TypedVals ~> freezerTypedValsHead(E) => E, HOLE ... [cool] + + syntax KItem ::= freezerAssignmentToArrayElementBase(Expression, Expression) + | freezerAssignmentToArrayElementIndex(Expression, Expression) + rule HOLE:Expression [ E2:Expression ] = E3:Expression => HOLE ~> freezerAssignmentToArrayElementBase(E2, E3) ... [heat] + rule HOLE:Expression ~> freezerAssignmentToArrayElementBase(E2, E3) => HOLE [ E2 ] = E3 ... [cool] + rule E1:Expression [ HOLE:Expression ] = E3:Expression => HOLE ~> freezerAssignmentToArrayElementIndex(E1, E3) ... [heat] + rule HOLE:Expression ~> freezerAssignmentToArrayElementIndex(E1, E3) => E1 [ HOLE ] = E3 ... [cool] + + syntax KItem ::= freezerCallElementaryTypeName(ElementaryTypeName) + rule T:ElementaryTypeName ( HOLE:CallArgumentList ) => HOLE ~> freezerCallElementaryTypeName(T) ... [heat] + rule HOLE:CallArgumentList ~> freezerCallElementaryTypeName(T) => T ( HOLE ) ... [cool] + + syntax KItem ::= freezerCallId(Id) + rule ID:Id ( HOLE:CallArgumentList ) => HOLE ~> freezerCallId(ID) ... [heat] + rule HOLE:CallArgumentList ~> freezerCallId(ID) => ID ( HOLE ) ... [cool] + + syntax KItem ::= freezerArrayElementLookupBase(Expression) + | freezerArrayElementLookupIndex(Expression) + rule HOLE:Expression [ E:Expression ] => HOLE ~> freezerArrayElementLookupBase(E) ... [heat] + rule HOLE:Expression ~> freezerArrayElementLookupBase(E) => HOLE [ E ] ... [cool] + rule E:Expression [ HOLE:Expression ] => HOLE ~> freezerArrayElementLookupIndex(E) ... [heat] + rule HOLE:Expression ~> freezerArrayElementLookupIndex(E) => E [ HOLE ] ... [cool] + + syntax KItem ::= freezerLength() + rule HOLE:Expression . length => HOLE ~> freezerLength() ... [heat] + rule HOLE:Expression ~> freezerLength() => HOLE . length ... [cool] + + syntax KItem ::= freezerExternalCallBase(Id, CallArgumentList) + | freezerExternalCallArgs(Expression, Id) + rule HOLE:Expression . ID:Id ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallBase(ID, ARGS) ... [heat] + rule HOLE:Expression ~> freezerExternalCallBase(ID, ARGS) => (HOLE . ID) ( ARGS ) ... [cool] + rule (E:Expression . ID:Id) ( HOLE:CallArgumentList ) => HOLE ~> freezerExternalCallArgs(E, ID) ... [heat] + rule HOLE:CallArgumentList ~> freezerExternalCallArgs(E, ID) => (E . ID) ( HOLE ) ... [cool] + + syntax KItem ::= freezerExternalCallWithValueBase(Id, Expression, CallArgumentList) + | freezerExternalCallWithValueValue(Expression, Id, CallArgumentList) + | freezerExternalCallWithValueArgs(Expression, Id, KeyValues) + rule HOLE:Expression . ID:Id { value: V:Expression } ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueBase(ID, V, ARGS) ... [heat] + rule HOLE:Expression ~> freezerExternalCallWithValueBase(ID, V, ARGS) => HOLE . ID { value : V } ( ARGS ) ... [cool] + rule E:Expression . ID:Id { value: HOLE:Expression } ( ARGS:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueValue(E, ID, ARGS) ... [heat] + rule HOLE:Expression ~> freezerExternalCallWithValueValue(E, ID, ARGS) => E . ID { value : HOLE } ( ARGS ) ... [cool] + rule E:Expression . ID:Id { L:KeyValues } ( HOLE:CallArgumentList ) => HOLE ~> freezerExternalCallWithValueArgs(E, ID, L) ... [heat] + rule HOLE:Expression ~> freezerExternalCallWithValueArgs(E, ID, L) => E . ID { L } ( HOLE ) ... [cool] + endmodule diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md index 994c693..25c8fce 100644 --- a/src/solidity-syntax.md +++ b/src/solidity-syntax.md @@ -179,23 +179,23 @@ In each code block, various statments and nested blocks can be present. Following is a list of supported statements. ```k - syntax ExpressionStatement ::= Expression ";" [strict] + syntax ExpressionStatement ::= Expression ";" syntax VariableDeclarationStatement ::= VariableDeclaration ";" - | VariableDeclaration "=" Expression ";" [strict(2)] - | "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)] + | VariableDeclaration "=" Expression ";" + | "(" VariableDeclaration "," ")" "=" Expression ";" - syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)] - | "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)] + syntax IfStatement ::= "if" "(" Expression ")" Statement + | "if" "(" Expression ")" Statement "else" Statement [avoid] syntax WhileStatement ::= "while" "(" Expression ")" Statement syntax Block ::= "for" "(" VariableDeclarationStatement Expression ";" Expression ")" Statement [function] rule for (Init Cond ; Post) Body => { Init while(Cond) { Body Post; } } - syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" [strict(2)] + syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" syntax ReturnStatement ::= "return" ";" - | "return" Expression ";" [strict] + | "return" Expression ";" syntax RevertStatement ::= "revert" "(" CallArgumentList ")" ";" | "revert" Id "(" CallArgumentList ")" ";" @@ -207,7 +207,7 @@ Following is a list of supported statements. `CallArgumentList` keeps a list of arguments for function calls and such (`revert()`, `emit()`, etc.) ```k - syntax CallArgumentList ::= List{Expression, ","} [overload(exps), strict] + syntax CallArgumentList ::= List{Expression, ","} [overload(exps)] ``` @@ -227,7 +227,7 @@ Following is a list of supported expressions. Operator precendences are taken fr syntax Expression ::= Id | Literal | LiteralWithSubDenom | ElementaryTypeName > "(" Expression ")" [bracket] | "[" CallArgumentList "]" - | "new" TypeName "(" CallArgumentList ")" [strict(2)] + | "new" TypeName "(" CallArgumentList ")" | Expression "++" | Expression "--" | Expression "[" Expression "]" | Expression "[""]" | Expression "." Id | Expression ".address" @@ -235,28 +235,27 @@ Following is a list of supported expressions. Operator precendences are taken fr | Expression "(" CallArgumentList ")" > "++" Expression | "--" Expression | "!" Expression - > left: Expression "**" Expression [strict] + > left: Expression "**" Expression > left: - Expression "*" Expression [strict] - | Expression "/" Expression [strict] - | Expression "%" Expression [strict] + Expression "*" Expression + | Expression "/" Expression + | Expression "%" Expression > left: - Expression "+" Expression [strict] - | Expression "-" Expression [strict] + Expression "+" Expression + | Expression "-" Expression > left: - Expression "<" Expression [strict] - | Expression "<=" Expression [strict] - | Expression ">" Expression [strict] - | Expression ">=" Expression [strict] + Expression "<" Expression + | Expression "<=" Expression + | Expression ">" Expression + | Expression ">=" Expression > left: - Expression "==" Expression [strict] - | Expression "!=" Expression [strict] - > left: Expression "&&" Expression [strict(1)] - > left: Expression "||" Expression [strict(1)] + Expression "==" Expression + | Expression "!=" Expression + > left: Expression "&&" Expression + > left: Expression "||" Expression > right: - Expression "?" Expression ":" Expression [strict(1)] - | Expression "=" Expression [strict(2)] - + Expression "?" Expression ":" Expression + | Expression "=" Expression endmodule ``` diff --git a/src/solidity.md b/src/solidity.md index 82ad844..d669866 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -100,7 +100,7 @@ module SOLIDITY-DATA-SYNTAX syntax Transactions ::= List{Transaction, ","} syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [function] - syntax Transaction ::= create(from: Decimal, value: Decimal, timestamp: Decimal, ctor: Id, args: CallArgumentList) [strict(5)] + syntax Transaction ::= create(from: Decimal, value: Decimal, timestamp: Decimal, ctor: Id, args: CallArgumentList) endmodule module SOLIDITY-DATA @@ -118,7 +118,7 @@ module SOLIDITY-DATA syntax Id ::= "constructor" [token] syntax TypedVal ::= v(Value, TypeName) | lv(BaseRef, List, TypeName) | Int | String | "void" - syntax TypedVals ::= List{TypedVal, ","} [overload(exps), strict] + syntax TypedVals ::= List{TypedVal, ","} [overload(exps)] syntax Expression ::= TypedVal syntax CallArgumentList ::= TypedVals syntax KResult ::= TypedVal | TypedVals diff --git a/src/statement.md b/src/statement.md index 9429205..66d56dd 100644 --- a/src/statement.md +++ b/src/statement.md @@ -88,4 +88,33 @@ module SOLIDITY-STATEMENT // while statement rule while (Cond) Body => if (Cond) {Body while(Cond) Body} else {.Statements} + // Heating and cooling rules + syntax KItem ::= freezerExpressionStatement() + rule HOLE:Expression ; => HOLE ~> freezerExpressionStatement() ... [heat] + rule HOLE:Expression ~> freezerExpressionStatement() => HOLE ; ... [cool] + + syntax KItem ::= freezerVariableDeclarationStatementA(VariableDeclaration) + rule D:VariableDeclaration = HOLE:Expression ; => HOLE ~> freezerVariableDeclarationStatementA(D) ... [heat] + rule HOLE:Expression ~> freezerVariableDeclarationStatementA(D) => D = HOLE ; ... [cool] + + syntax KItem ::= freezerVariableDeclarationStatementB(VariableDeclaration) + rule ( D:VariableDeclaration , ) = HOLE:Expression ; => HOLE ~> freezerVariableDeclarationStatementB(D) ... [heat] + rule HOLE:Expression ~> freezerVariableDeclarationStatementB(D) => ( D , ) = HOLE ; ... [cool] + + syntax KItem ::= freezerIfStatement(Statement) + rule if ( HOLE:Expression ) S:Statement => HOLE ~> freezerIfStatement(S) ... [heat] + rule HOLE:Expression ~> freezerIfStatement(S) => if ( HOLE ) S ... [cool] + + syntax KItem ::= freezerIfElseStatement(Statement, Statement) + rule if ( HOLE:Expression ) S1:Statement else S2:Statement => HOLE ~> freezerIfElseStatement(S1, S2) ... [heat] + rule HOLE:Expression ~> freezerIfElseStatement(S1, S2) => if ( HOLE ) S1 else S2 ... [cool] + + syntax KItem ::= freezerEmitStatement(Expression) + rule emit E:Expression ( HOLE:CallArgumentList ) ; => HOLE ~> freezerEmitStatement(E) ... [heat] + rule HOLE ~> freezerEmitStatement(E) => emit E ( HOLE ) ; ... [cool] + + syntax KItem ::= freezerReturnStatement() + rule return HOLE:Expression ; => HOLE ~> freezerReturnStatement() ... [heat] + rule HOLE:Expression ~> freezerReturnStatement() => return HOLE ; ... [cool] + endmodule diff --git a/src/transaction.md b/src/transaction.md index 20ac437..1ff8a57 100644 --- a/src/transaction.md +++ b/src/transaction.md @@ -57,7 +57,7 @@ module SOLIDITY-TRANSACTION ADDR => ADDR +MInt 1p160 [owise] - syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)] + syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS) rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ... @@ -82,4 +82,11 @@ module SOLIDITY-TRANSACTION BODY requires isKResult(ARGS) + syntax KItem ::= freezerTransactionCreate(Decimal, Decimal, Decimal, Id) + | freezerTransactionTxn(Decimal, MInt{160}, Decimal, Decimal, Id) + rule create(FROM, VALUE, NOW, CTOR, HOLE:CallArgumentList) => HOLE ~> freezerTransactionCreate(FROM, VALUE, NOW, CTOR) ... [heat] + rule HOLE ~> freezerTransactionCreate(FROM, VALUE, NOW, CTOR) => create(FROM, VALUE, NOW, CTOR, HOLE) ... [cool] + rule txn(FROM, TO, VALUE, NOW, FUNC, HOLE:CallArgumentList) => HOLE ~> freezerTransactionTxn(FROM, TO, VALUE, NOW, FUNC) ... [heat] + rule HOLE:CallArgumentList ~> freezerTransactionTxn(FROM, TO, VALUE, NOW, FUNC) => txn(FROM, TO, VALUE, NOW, FUNC, HOLE) ... [cool] + endmodule diff --git a/test/regression/funcnamefail.ref b/test/regression/funcnamefail.ref index 05f7414..396df8f 100644 --- a/test/regression/funcnamefail.ref +++ b/test/regression/funcnamefail.ref @@ -1,6 +1,6 @@ - require ( v ( false , bool ) , "" , .TypedVals ) ~> #freezer_;_SOLIDITY-SYNTAX_ExpressionStatement_Expression0_ ( ) ~> return 2 ; .Statements ~> return void ; ~> .K + require ( v ( false , bool ) , "" , .TypedVals ) ~> freezerExpressionStatement ( ) ~> return 2 ; .Statements ~> return void ; ~> .K false @@ -136,8 +136,8 @@ chaincall2 - ListItem ( frame (... continuation: #freezer_=_;_SOLIDITY-SYNTAX_VariableDeclarationStatement_VariableDeclaration_Expression1_ ( uint256 x ~> .K ) ~> .Statements ~> .Transactions ~> .K , env: .Map , func: constructor ) ) - ListItem ( frame (... continuation: #freezerreturn_;_SOLIDITY-SYNTAX_ReturnStatement_Expression0_ ( ) ~> .Statements ~> return void ; ~> .K , env: .Map , func: chaincall1 ) ) + ListItem ( frame (... continuation: freezerVariableDeclarationStatementA ( uint256 x ) ~> .Statements ~> .Transactions ~> .K , env: .Map , func: constructor ) ) + ListItem ( frame (... continuation: freezerReturnStatement ( ) ~> .Statements ~> return void ; ~> .K , env: .Map , func: chaincall1 ) )