diff --git a/src/instrumenter/interpose.ts b/src/instrumenter/interpose.ts index 2e9bee33..4f6c95f2 100644 --- a/src/instrumenter/interpose.ts +++ b/src/instrumenter/interpose.ts @@ -24,6 +24,7 @@ import { PointerType, specializeType, StateVariableVisibility, + SuperType, TypeName, TypeNode, UserDefinedType, @@ -403,37 +404,42 @@ export function interposeCall( const params: VariableDeclaration[] = []; const returns: VariableDeclaration[] = []; - let receiver: Expression; + let receiver: Expression | undefined; let callOriginalExp: Expression; const baseT = ctx.typeEnv.inference.typeOf(callee.vExpression); if (call.vFunctionCallType === ExternalReferenceType.UserDefined) { - assert( - baseT instanceof UserDefinedType && baseT.definition instanceof ContractDefinition, - "Expected base to be a reference to a contract, not {0}", - baseT - ); - - params.push( - factory.makeVariableDeclaration( - false, - false, - "receiver", - wrapper.id, - false, - DataLocation.Default, - StateVariableVisibility.Default, - Mutability.Mutable, - baseT.pp(), - undefined, - factory.makeUserDefinedTypeName( - "", - getFQName(baseT.definition, call), - baseT.definition.id + if (baseT instanceof UserDefinedType && baseT.definition instanceof ContractDefinition) { + params.push( + factory.makeVariableDeclaration( + false, + false, + "receiver", + wrapper.id, + false, + DataLocation.Default, + StateVariableVisibility.Default, + Mutability.Mutable, + baseT.pp(), + undefined, + factory.makeUserDefinedTypeName( + "", + getFQName(baseT.definition, call), + baseT.definition.id + ) ) - ) - ); + ); + + receiver = factory.copy(callee.vExpression); + copySrc(callee.vExpression, receiver); + } else { + assert( + baseT instanceof SuperType, + "Expected base to be a reference to a contract or super, not {0}", + baseT + ); + } params.push( ...calleeT.parameters.map((paramT, idx) => { @@ -459,12 +465,11 @@ export function interposeCall( ) ); - receiver = factory.copy(callee.vExpression); - copySrc(callee.vExpression, receiver); - callOriginalExp = factory.makeMemberAccess( call.vExpression.typeString, - factory.makeIdentifierFor(params[0]), + baseT instanceof SuperType + ? factory.makeIdentifier("", "super", -1) + : factory.makeIdentifierFor(params[0]), callee.memberName, callee.referencedDeclaration ); @@ -554,7 +559,7 @@ export function interposeCall( ); } - let nImplicitArgs = 1; + let nImplicitArgs = baseT instanceof SuperType ? 0 : 1; /** * If the original call had gas/value function call options, we need @@ -644,7 +649,8 @@ export function interposeCall( contract.appendChild(wrapper); call.vExpression = newCallee; - call.vArguments.unshift(receiver); + + if (receiver) call.vArguments.unshift(receiver); // If the call is in a pure/view function change its mutability const containingFun = getScopeFun(call); diff --git a/test/samples/hardhat_test.instrumented.sol b/test/samples/hardhat_test.instrumented.sol index 9c47c9d5..9cfe6b0f 100644 --- a/test/samples/hardhat_test.instrumented.sol +++ b/test/samples/hardhat_test.instrumented.sol @@ -218,7 +218,7 @@ contract HardHatTest { } { console.logString("HIT: 007987:0040:000 6: "); - if (!(__ScribbleUtilsLib__18.eq_encoded(abi.encode(str), "abc"))) { + if (!(__ScribbleUtilsLib__19.eq_encoded(abi.encode(str), "abc"))) { console.logString("str"); console.logString(str); console.logString("007987:0040:000 6: "); @@ -227,7 +227,7 @@ contract HardHatTest { } { console.logString("HIT: 008360:0040:000 7: "); - if (!(__ScribbleUtilsLib__18.eq_encoded(bts, hex"010203"))) { + if (!(__ScribbleUtilsLib__19.eq_encoded(bts, hex"010203"))) { console.logString("bts"); console.logBytes(bts); console.logString("008360:0040:000 7: "); @@ -539,7 +539,7 @@ contract HardHatTest { function _original_HardHatTest_main(string memory str, bytes memory bts) private {} } -library __ScribbleUtilsLib__18 { +library __ScribbleUtilsLib__19 { function isInContract() internal returns (bool res) { assembly { res := sload(0x5f0b92cf9616afdee4f4136f66393f1343b027f01be893fa569eb2e2b667a40c) diff --git a/test/samples/hardhat_test.sol b/test/samples/hardhat_test.sol index 39393595..9cb8b352 100644 --- a/test/samples/hardhat_test.sol +++ b/test/samples/hardhat_test.sol @@ -1,3 +1,4 @@ +pragma solidity 0.8.21; contract HardHatTest { uint8[] b = [1, 2, 3]; diff --git a/test/samples/immutables.instrumented.sol b/test/samples/immutables.instrumented.sol index 3ae13d97..7f520cd2 100644 --- a/test/samples/immutables.instrumented.sol +++ b/test/samples/immutables.instrumented.sol @@ -1,6 +1,6 @@ /// This file is auto-generated by Scribble and shouldn't be edited directly. /// Use --disarm prior to make any changes. -pragma solidity 0.8.21; +pragma solidity 0.8.20; /// #if_succeeds x == 5; contract Example01 { @@ -10,7 +10,7 @@ contract Example01 { x = 5; unchecked { if (!(x == 5)) { - emit __ScribbleUtilsLib__55.AssertionFailed("000324:0066:000 0: "); + emit __ScribbleUtilsLib__56.AssertionFailed("000324:0066:000 0: "); assert(false); } } @@ -25,7 +25,7 @@ contract Example02 { x = 5; unchecked { if (!(x == 5)) { - emit __ScribbleUtilsLib__55.AssertionFailed("000637:0066:000 1: "); + emit __ScribbleUtilsLib__56.AssertionFailed("000637:0066:000 1: "); assert(false); } } @@ -58,7 +58,7 @@ contract Example04 { } } -library __ScribbleUtilsLib__55 { +library __ScribbleUtilsLib__56 { event AssertionFailed(string message); event AssertionFailedData(int eventId, bytes encodingData); diff --git a/test/samples/immutables.sol b/test/samples/immutables.sol index 54c42461..b6fc2eea 100644 --- a/test/samples/immutables.sol +++ b/test/samples/immutables.sol @@ -1,3 +1,4 @@ +pragma solidity 0.8.20; /// #if_succeeds x == 5; contract Example01 { uint private immutable x; diff --git a/test/samples/immutables.sol.json b/test/samples/immutables.sol.json index 3fa6ddd6..19b3f7dc 100644 --- a/test/samples/immutables.sol.json +++ b/test/samples/immutables.sol.json @@ -1 +1 @@ -{"sources":{"test/samples/immutables.sol":{"ast":{"absolutePath":"test/samples/immutables.sol","exportedSymbols":{"Example01":[12],"Example02":[24],"Example03":[39],"Example04":[54]},"id":55,"nodeType":"SourceUnit","nodes":[{"abstract":false,"baseContracts":[],"canonicalName":"Example01","contractDependencies":[],"contractKind":"contract","documentation":{"id":1,"nodeType":"StructuredDocumentation","src":"0:25:0","text":"#if_succeeds x == 5;"},"fullyImplemented":true,"id":12,"linearizedBaseContracts":[12],"name":"Example01","nameLocation":"34:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":3,"mutability":"immutable","name":"x","nameLocation":"73:1:0","nodeType":"VariableDeclaration","scope":12,"src":"50:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":2,"name":"uint","nodeType":"ElementaryTypeName","src":"50:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"body":{"id":10,"nodeType":"Block","src":"95:22:0","statements":[{"expression":{"id":8,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":6,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":3,"src":"105:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":7,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"109:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"105:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":9,"nodeType":"ExpressionStatement","src":"105:5:0"}]},"id":11,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":4,"nodeType":"ParameterList","parameters":[],"src":"92:2:0"},"returnParameters":{"id":5,"nodeType":"ParameterList","parameters":[],"src":"95:0:0"},"scope":12,"src":"81:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":55,"src":"25:94:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example02","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":24,"linearizedBaseContracts":[24],"name":"Example02","nameLocation":"130:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":14,"mutability":"immutable","name":"x","nameLocation":"169:1:0","nodeType":"VariableDeclaration","scope":24,"src":"146:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":13,"name":"uint","nodeType":"ElementaryTypeName","src":"146:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"body":{"id":22,"nodeType":"Block","src":"220:22:0","statements":[{"expression":{"id":20,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":18,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":14,"src":"230:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":19,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"234:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"230:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":21,"nodeType":"ExpressionStatement","src":"230:5:0"}]},"documentation":{"id":15,"nodeType":"StructuredDocumentation","src":"177:24:0","text":"#if_succeeds x == 5;"},"id":23,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":16,"nodeType":"ParameterList","parameters":[],"src":"217:2:0"},"returnParameters":{"id":17,"nodeType":"ParameterList","parameters":[],"src":"220:0:0"},"scope":24,"src":"206:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":55,"src":"121:123:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example03","contractDependencies":[],"contractKind":"contract","documentation":{"id":25,"nodeType":"StructuredDocumentation","src":"246:21:0","text":"#require y == 1;"},"fullyImplemented":true,"id":39,"linearizedBaseContracts":[39],"name":"Example03","nameLocation":"276:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":27,"mutability":"immutable","name":"x","nameLocation":"315:1:0","nodeType":"VariableDeclaration","scope":39,"src":"292:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":26,"name":"uint","nodeType":"ElementaryTypeName","src":"292:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"constant":false,"id":30,"mutability":"mutable","name":"y","nameLocation":"327:1:0","nodeType":"VariableDeclaration","scope":39,"src":"322:10:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":28,"name":"uint","nodeType":"ElementaryTypeName","src":"322:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"value":{"hexValue":"31","id":29,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"331:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"visibility":"internal"},{"body":{"id":37,"nodeType":"Block","src":"353:22:0","statements":[{"expression":{"id":35,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":33,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":27,"src":"363:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":34,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"367:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"363:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":36,"nodeType":"ExpressionStatement","src":"363:5:0"}]},"id":38,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":31,"nodeType":"ParameterList","parameters":[],"src":"350:2:0"},"returnParameters":{"id":32,"nodeType":"ParameterList","parameters":[],"src":"353:0:0"},"scope":39,"src":"339:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":55,"src":"267:110:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example04","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":54,"linearizedBaseContracts":[54],"name":"Example04","nameLocation":"388:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":41,"mutability":"immutable","name":"x","nameLocation":"427:1:0","nodeType":"VariableDeclaration","scope":54,"src":"404:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":40,"name":"uint","nodeType":"ElementaryTypeName","src":"404:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"constant":false,"id":44,"mutability":"mutable","name":"y","nameLocation":"439:1:0","nodeType":"VariableDeclaration","scope":54,"src":"434:10:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":42,"name":"uint","nodeType":"ElementaryTypeName","src":"434:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"value":{"hexValue":"31","id":43,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"443:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"visibility":"internal"},{"body":{"id":52,"nodeType":"Block","src":"490:22:0","statements":[{"expression":{"id":50,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":48,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":41,"src":"500:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":49,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"504:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"500:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":51,"nodeType":"ExpressionStatement","src":"500:5:0"}]},"documentation":{"id":45,"nodeType":"StructuredDocumentation","src":"451:20:0","text":"#require y == 1;"},"id":53,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":46,"nodeType":"ParameterList","parameters":[],"src":"487:2:0"},"returnParameters":{"id":47,"nodeType":"ParameterList","parameters":[],"src":"490:0:0"},"scope":54,"src":"476:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":55,"src":"379:135:0","usedErrors":[],"usedEvents":[]}],"src":"25:492:0","sourceEntryKey":"test/samples/immutables.sol"},"id":0,"source":"/// #if_succeeds x == 5;\ncontract Example01 {\n uint private immutable x;\n\n constructor() {\n x = 5;\n }\n}\n\ncontract Example02 {\n uint private immutable x;\n\n /// #if_succeeds x == 5;\n constructor() {\n x = 5;\n }\n}\n\n/// #require y == 1;\ncontract Example03 {\n uint private immutable x;\n uint y = 1;\n\n constructor() {\n x = 5;\n }\n}\n\ncontract Example04 {\n uint private immutable x;\n uint y = 1;\n\n /// #require y == 1;\n constructor() {\n x = 5;\n }\n}\n\n\n"}},"compilerVersion":"0.8.21"} \ No newline at end of file +{"sources":{"test/samples/immutables.sol":{"ast":{"absolutePath":"test/samples/immutables.sol","exportedSymbols":{"Example01":[13],"Example02":[25],"Example03":[40],"Example04":[55]},"id":56,"nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity","0.8",".20"],"nodeType":"PragmaDirective","src":"0:23:0"},{"abstract":false,"baseContracts":[],"canonicalName":"Example01","contractDependencies":[],"contractKind":"contract","documentation":{"id":2,"nodeType":"StructuredDocumentation","src":"24:25:0","text":"#if_succeeds x == 5;"},"fullyImplemented":true,"id":13,"linearizedBaseContracts":[13],"name":"Example01","nameLocation":"58:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":4,"mutability":"immutable","name":"x","nameLocation":"97:1:0","nodeType":"VariableDeclaration","scope":13,"src":"74:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":3,"name":"uint","nodeType":"ElementaryTypeName","src":"74:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"body":{"id":11,"nodeType":"Block","src":"119:22:0","statements":[{"expression":{"id":9,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":7,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":4,"src":"129:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":8,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"133:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"129:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":10,"nodeType":"ExpressionStatement","src":"129:5:0"}]},"id":12,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":5,"nodeType":"ParameterList","parameters":[],"src":"116:2:0"},"returnParameters":{"id":6,"nodeType":"ParameterList","parameters":[],"src":"119:0:0"},"scope":13,"src":"105:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":56,"src":"49:94:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example02","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":25,"linearizedBaseContracts":[25],"name":"Example02","nameLocation":"154:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":15,"mutability":"immutable","name":"x","nameLocation":"193:1:0","nodeType":"VariableDeclaration","scope":25,"src":"170:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":14,"name":"uint","nodeType":"ElementaryTypeName","src":"170:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"body":{"id":23,"nodeType":"Block","src":"244:22:0","statements":[{"expression":{"id":21,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":19,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":15,"src":"254:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":20,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"258:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"254:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":22,"nodeType":"ExpressionStatement","src":"254:5:0"}]},"documentation":{"id":16,"nodeType":"StructuredDocumentation","src":"201:24:0","text":"#if_succeeds x == 5;"},"id":24,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":17,"nodeType":"ParameterList","parameters":[],"src":"241:2:0"},"returnParameters":{"id":18,"nodeType":"ParameterList","parameters":[],"src":"244:0:0"},"scope":25,"src":"230:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":56,"src":"145:123:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example03","contractDependencies":[],"contractKind":"contract","documentation":{"id":26,"nodeType":"StructuredDocumentation","src":"270:21:0","text":"#require y == 1;"},"fullyImplemented":true,"id":40,"linearizedBaseContracts":[40],"name":"Example03","nameLocation":"300:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":28,"mutability":"immutable","name":"x","nameLocation":"339:1:0","nodeType":"VariableDeclaration","scope":40,"src":"316:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":27,"name":"uint","nodeType":"ElementaryTypeName","src":"316:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"constant":false,"id":31,"mutability":"mutable","name":"y","nameLocation":"351:1:0","nodeType":"VariableDeclaration","scope":40,"src":"346:10:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":29,"name":"uint","nodeType":"ElementaryTypeName","src":"346:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"value":{"hexValue":"31","id":30,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"355:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"visibility":"internal"},{"body":{"id":38,"nodeType":"Block","src":"377:22:0","statements":[{"expression":{"id":36,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":34,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":28,"src":"387:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":35,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"391:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"387:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":37,"nodeType":"ExpressionStatement","src":"387:5:0"}]},"id":39,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":32,"nodeType":"ParameterList","parameters":[],"src":"374:2:0"},"returnParameters":{"id":33,"nodeType":"ParameterList","parameters":[],"src":"377:0:0"},"scope":40,"src":"363:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":56,"src":"291:110:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"Example04","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":55,"linearizedBaseContracts":[55],"name":"Example04","nameLocation":"412:9:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":42,"mutability":"immutable","name":"x","nameLocation":"451:1:0","nodeType":"VariableDeclaration","scope":55,"src":"428:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":41,"name":"uint","nodeType":"ElementaryTypeName","src":"428:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"private"},{"constant":false,"id":45,"mutability":"mutable","name":"y","nameLocation":"463:1:0","nodeType":"VariableDeclaration","scope":55,"src":"458:10:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":43,"name":"uint","nodeType":"ElementaryTypeName","src":"458:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"value":{"hexValue":"31","id":44,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"467:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"visibility":"internal"},{"body":{"id":53,"nodeType":"Block","src":"514:22:0","statements":[{"expression":{"id":51,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":49,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":42,"src":"524:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"35","id":50,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"528:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},"src":"524:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":52,"nodeType":"ExpressionStatement","src":"524:5:0"}]},"documentation":{"id":46,"nodeType":"StructuredDocumentation","src":"475:20:0","text":"#require y == 1;"},"id":54,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":47,"nodeType":"ParameterList","parameters":[],"src":"511:2:0"},"returnParameters":{"id":48,"nodeType":"ParameterList","parameters":[],"src":"514:0:0"},"scope":55,"src":"500:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":56,"src":"403:135:0","usedErrors":[],"usedEvents":[]}],"src":"0:541:0","sourceEntryKey":"test/samples/immutables.sol"},"id":0,"source":"pragma solidity 0.8.20;\n/// #if_succeeds x == 5;\ncontract Example01 {\n uint private immutable x;\n\n constructor() {\n x = 5;\n }\n}\n\ncontract Example02 {\n uint private immutable x;\n\n /// #if_succeeds x == 5;\n constructor() {\n x = 5;\n }\n}\n\n/// #require y == 1;\ncontract Example03 {\n uint private immutable x;\n uint y = 1;\n\n constructor() {\n x = 5;\n }\n}\n\ncontract Example04 {\n uint private immutable x;\n uint y = 1;\n\n /// #require y == 1;\n constructor() {\n x = 5;\n }\n}\n\n\n"}},"compilerVersion":"0.8.20"} \ No newline at end of file diff --git a/test/samples/predefined.instrumented.sol b/test/samples/predefined.instrumented.sol index c01b9576..20e56627 100644 --- a/test/samples/predefined.instrumented.sol +++ b/test/samples/predefined.instrumented.sol @@ -1,20 +1,20 @@ /// This file is auto-generated by Scribble and shouldn't be edited directly. /// Use --disarm prior to make any changes. -pragma solidity 0.8.21; +pragma solidity 0.8.20; /// #const uint256 H := 60 * 60; /// #const uint256 D := H * 24; contract A { /// Definition of user constant const uint256 H := (60 * 60) - uint256 internal H_7_0; + uint256 internal H_8_0; /// Definition of user constant const uint256 D := (H * 24) - uint256 internal D_7_0; + uint256 internal D_8_0; function testHD() public { _original_A_testHD(); unchecked { - if (!(D_7_0 == (H_7_0 * 24))) { - emit __ScribbleUtilsLib__97.AssertionFailed("000553:0066:000 2: "); + if (!(D_8_0 == (H_8_0 * 24))) { + emit __ScribbleUtilsLib__98.AssertionFailed("000553:0066:000 2: "); assert(false); } } @@ -24,9 +24,9 @@ contract A { constructor() { /// Value assignment for const uint256 H := (60 * 60) - H_7_0 = 60 * 60; + H_8_0 = 60 * 60; /// Value assignment for const uint256 D := (H * 24) - D_7_0 = H_7_0 * 24; + D_8_0 = H_8_0 * 24; } } @@ -35,17 +35,17 @@ contract A { /// #const uint256 W := D * 7; contract B { /// Definition of user constant const uint256 H := (60 * 60) - uint256 internal H_14_0; + uint256 internal H_15_0; /// Definition of user constant const uint256 D := (H * 24) - uint256 internal D_14_0; + uint256 internal D_15_0; /// Definition of user constant const uint256 W := (D * 7) - uint256 internal W_14_0; + uint256 internal W_15_0; function testWHD() public { _original_B_testWHD(); unchecked { - if (!(((W_14_0 == (D_14_0 * 7)) && (D_14_0 == (H_14_0 * 24))) && (H_14_0 == (60 * 60)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("001527:0066:000 6: "); + if (!(((W_15_0 == (D_15_0 * 7)) && (D_15_0 == (H_15_0 * 24))) && (H_15_0 == (60 * 60)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("001527:0066:000 6: "); assert(false); } } @@ -55,11 +55,11 @@ contract B { constructor() { /// Value assignment for const uint256 H := (60 * 60) - H_14_0 = 60 * 60; + H_15_0 = 60 * 60; /// Value assignment for const uint256 D := (H * 24) - D_14_0 = H_14_0 * 24; + D_15_0 = H_15_0 * 24; /// Value assignment for const uint256 W := (D * 7) - W_14_0 = D_14_0 * 7; + W_15_0 = D_15_0 * 7; } } @@ -146,48 +146,48 @@ contract EqEncoded { function positive() public returns (bool RET_0) { RET_0 = _original_EqEncoded_positive(); unchecked { - if (!(__ScribbleUtilsLib__97.eq_encoded("abc", hex"616263"))) { - emit __ScribbleUtilsLib__97.AssertionFailed("004445:0067:000 14: "); + if (!(__ScribbleUtilsLib__98.eq_encoded("abc", hex"616263"))) { + emit __ScribbleUtilsLib__98.AssertionFailed("004445:0067:000 14: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(bytes2(0xffcc)), abi.encode(bytes2(0xffcc))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("004687:0067:000 15: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(bytes2(0xffcc)), abi.encode(bytes2(0xffcc))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("004687:0067:000 15: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000), abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("004985:0067:000 16: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000), abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("004985:0067:000 16: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(uint256(512)), abi.encode(uint16(512))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("005222:0067:000 17: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(uint256(512)), abi.encode(uint16(512))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("005222:0067:000 17: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(int256(-512)), abi.encode(int256(-512))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("005460:0067:000 18: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(int256(-512)), abi.encode(int256(-512))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("005460:0067:000 18: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(true), abi.encode(true)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("005682:0067:000 19: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(true), abi.encode(true)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("005682:0067:000 19: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(false), abi.encode(false)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("005906:0067:000 20: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(false), abi.encode(false)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("005906:0067:000 20: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(Some(1)), abi.encode(s)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("006128:0067:000 21: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(Some(1)), abi.encode(s)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("006128:0067:000 21: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(Other.A), abi.encode(Other.A)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("006356:0067:000 22: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(Other.A), abi.encode(Other.A)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("006356:0067:000 22: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(a), abi.encode(b)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("006572:0067:000 23: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(a), abi.encode(b)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("006572:0067:000 23: "); assert(false); } - if (!(__ScribbleUtilsLib__97.eq_encoded(abi.encode(d), abi.encode(e)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("006788:0067:000 24: "); + if (!(__ScribbleUtilsLib__98.eq_encoded(abi.encode(d), abi.encode(e)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("006788:0067:000 24: "); assert(false); } } @@ -200,52 +200,52 @@ contract EqEncoded { function negative() public returns (bool RET_0) { RET_0 = _original_EqEncoded_negative(); unchecked { - if (!(!__ScribbleUtilsLib__97.eq_encoded("abc", "abcd"))) { - emit __ScribbleUtilsLib__97.AssertionFailed("007226:0067:000 25: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded("abc", "abcd"))) { + emit __ScribbleUtilsLib__98.AssertionFailed("007226:0067:000 25: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded("abc", "def"))) { - emit __ScribbleUtilsLib__97.AssertionFailed("007427:0067:000 26: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded("abc", "def"))) { + emit __ScribbleUtilsLib__98.AssertionFailed("007427:0067:000 26: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(hex"616263", hex"616264"))) { - emit __ScribbleUtilsLib__97.AssertionFailed("007640:0067:000 27: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(hex"616263", hex"616264"))) { + emit __ScribbleUtilsLib__98.AssertionFailed("007640:0067:000 27: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(bytes2(0xffcc)), abi.encode(bytes2(0xffff))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("007883:0067:000 28: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(bytes2(0xffcc)), abi.encode(bytes2(0xffff))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("007883:0067:000 28: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF), abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("008182:0067:000 29: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF), abi.encode(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("008182:0067:000 29: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(uint256(512)), abi.encode(uint16(1024))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("008421:0067:000 30: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(uint256(512)), abi.encode(uint16(1024))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("008421:0067:000 30: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(int256(-512)), abi.encode(int256(-1024))))) { - emit __ScribbleUtilsLib__97.AssertionFailed("008661:0067:000 31: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(int256(-512)), abi.encode(int256(-1024))))) { + emit __ScribbleUtilsLib__98.AssertionFailed("008661:0067:000 31: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(true), abi.encode(false)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("008885:0067:000 32: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(true), abi.encode(false)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("008885:0067:000 32: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(Some(2)), abi.encode(s)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("009108:0067:000 33: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(Some(2)), abi.encode(s)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("009108:0067:000 33: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(Other.A), abi.encode(Other.B)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("009337:0067:000 34: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(Other.A), abi.encode(Other.B)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("009337:0067:000 34: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(a), abi.encode(d)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("009554:0067:000 35: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(a), abi.encode(d)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("009554:0067:000 35: "); assert(false); } - if (!(!__ScribbleUtilsLib__97.eq_encoded(abi.encode(c), abi.encode(f)))) { - emit __ScribbleUtilsLib__97.AssertionFailed("009771:0067:000 36: "); + if (!(!__ScribbleUtilsLib__98.eq_encoded(abi.encode(c), abi.encode(f)))) { + emit __ScribbleUtilsLib__98.AssertionFailed("009771:0067:000 36: "); assert(false); } } @@ -256,7 +256,7 @@ contract EqEncoded { } } -library __ScribbleUtilsLib__97 { +library __ScribbleUtilsLib__98 { event AssertionFailed(string message); event AssertionFailedData(int eventId, bytes encodingData); @@ -291,8 +291,8 @@ contract C is B { /// #if_succeeds old(W) == D * 7; constructor() { unchecked { - if (!(W_14_0 == (D_14_0 * 7))) { - emit __ScribbleUtilsLib__97.AssertionFailed("011083:0066:000 7: "); + if (!(W_15_0 == (D_15_0 * 7))) { + emit __ScribbleUtilsLib__98.AssertionFailed("011083:0066:000 7: "); assert(false); } } diff --git a/test/samples/predefined.sol b/test/samples/predefined.sol index 4fbe0846..9ad7bd5b 100644 --- a/test/samples/predefined.sol +++ b/test/samples/predefined.sol @@ -1,3 +1,4 @@ +pragma solidity 0.8.20; /// #const uint256 H := 60 * 60; /// #const uint256 D := H * 24; contract A { diff --git a/test/samples/predefined.sol.json b/test/samples/predefined.sol.json index 879cb660..40cf00a9 100644 --- a/test/samples/predefined.sol.json +++ b/test/samples/predefined.sol.json @@ -1 +1 @@ -{"sources":{"test/samples/predefined.sol":{"ast":{"absolutePath":"test/samples/predefined.sol","exportedSymbols":{"A":[7],"B":[14],"C":[22],"EqEncoded":[96],"UserDefinedFunctions":[26]},"id":97,"nodeType":"SourceUnit","nodes":[{"abstract":false,"baseContracts":[],"canonicalName":"A","contractDependencies":[],"contractKind":"contract","documentation":{"id":1,"nodeType":"StructuredDocumentation","src":"0:65:0","text":"#const uint256 H := 60 * 60;\n #const uint256 D := H * 24;"},"fullyImplemented":true,"id":7,"linearizedBaseContracts":[7],"name":"A","nameLocation":"74:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":5,"nodeType":"Block","src":"141:2:0","statements":[]},"documentation":{"id":2,"nodeType":"StructuredDocumentation","src":"82:29:0","text":"#if_succeeds D == H * 24;"},"functionSelector":"540cffdc","id":6,"implemented":true,"kind":"function","modifiers":[],"name":"testHD","nameLocation":"125:6:0","nodeType":"FunctionDefinition","parameters":{"id":3,"nodeType":"ParameterList","parameters":[],"src":"131:2:0"},"returnParameters":{"id":4,"nodeType":"ParameterList","parameters":[],"src":"141:0:0"},"scope":7,"src":"116:27:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":97,"src":"65:80:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"B","contractDependencies":[],"contractKind":"contract","documentation":{"id":8,"nodeType":"StructuredDocumentation","src":"147:96:0","text":"#const uint256 H := 60 * 60;\n #const uint256 D := H * 24;\n #const uint256 W := D * 7;"},"fullyImplemented":true,"id":14,"linearizedBaseContracts":[14],"name":"B","nameLocation":"252:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":12,"nodeType":"Block","src":"350:2:0","statements":[]},"documentation":{"id":9,"nodeType":"StructuredDocumentation","src":"260:59:0","text":"#if_succeeds W == D * 7 && D == H * 24 && H == 60 * 60;"},"functionSelector":"3bf401bc","id":13,"implemented":true,"kind":"function","modifiers":[],"name":"testWHD","nameLocation":"333:7:0","nodeType":"FunctionDefinition","parameters":{"id":10,"nodeType":"ParameterList","parameters":[],"src":"340:2:0"},"returnParameters":{"id":11,"nodeType":"ParameterList","parameters":[],"src":"350:0:0"},"scope":14,"src":"324:28:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":97,"src":"243:111:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[{"baseName":{"id":15,"name":"B","nameLocations":["370:1:0"],"nodeType":"IdentifierPath","referencedDeclaration":14,"src":"370:1:0"},"id":16,"nodeType":"InheritanceSpecifier","src":"370:1:0"}],"canonicalName":"C","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":22,"linearizedBaseContracts":[22,14],"name":"C","nameLocation":"365:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":20,"nodeType":"Block","src":"430:2:0","statements":[]},"documentation":{"id":17,"nodeType":"StructuredDocumentation","src":"378:33:0","text":"#if_succeeds old(W) == D * 7;"},"id":21,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":18,"nodeType":"ParameterList","parameters":[],"src":"427:2:0"},"returnParameters":{"id":19,"nodeType":"ParameterList","parameters":[],"src":"430:0:0"},"scope":22,"src":"416:16:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":97,"src":"356:78:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"UserDefinedFunctions","contractDependencies":[],"contractKind":"contract","documentation":{"id":23,"nodeType":"StructuredDocumentation","src":"485:283:0","text":"#define plus(uint x) uint = z + x;\n #define plus2(uint Foo) uint = z + Foo;\n #define plus3(uint plus2) uint = z + plus2;\n #define double(uint z) uint = z+z;\n #define quad(uint z) uint = let res := z+z in res + res;\n #define quad2(uint z) uint = double(double(z));"},"fullyImplemented":true,"id":26,"linearizedBaseContracts":[26],"name":"UserDefinedFunctions","nameLocation":"777:20:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":25,"mutability":"mutable","name":"z","nameLocation":"806:1:0","nodeType":"VariableDeclaration","scope":26,"src":"801:6:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":24,"name":"uint","nodeType":"ElementaryTypeName","src":"801:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"scope":97,"src":"768:42:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"EqEncoded","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":96,"linearizedBaseContracts":[96],"name":"EqEncoded","nameLocation":"870:9:0","nodeType":"ContractDefinition","nodes":[{"canonicalName":"EqEncoded.Some","id":29,"members":[{"constant":false,"id":28,"mutability":"mutable","name":"a","nameLocation":"913:1:0","nodeType":"VariableDeclaration","scope":29,"src":"908:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":27,"name":"uint","nodeType":"ElementaryTypeName","src":"908:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"name":"Some","nameLocation":"893:4:0","nodeType":"StructDefinition","scope":96,"src":"886:35:0","visibility":"public"},{"canonicalName":"EqEncoded.Other","id":32,"members":[{"id":30,"name":"A","nameLocation":"948:1:0","nodeType":"EnumValue","src":"948:1:0"},{"id":31,"name":"B","nameLocation":"951:1:0","nodeType":"EnumValue","src":"951:1:0"}],"name":"Other","nameLocation":"932:5:0","nodeType":"EnumDefinition","src":"927:31:0"},{"constant":false,"id":40,"mutability":"mutable","name":"a","nameLocation":"975:1:0","nodeType":"VariableDeclaration","scope":96,"src":"964:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":33,"name":"uint256","nodeType":"ElementaryTypeName","src":"964:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":35,"length":{"hexValue":"33","id":34,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"972:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"964:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"components":[{"hexValue":"31","id":36,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"980:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},{"hexValue":"32","id":37,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"983:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},{"hexValue":"33","id":38,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"986:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"}],"id":39,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"979:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":48,"mutability":"mutable","name":"b","nameLocation":"1005:1:0","nodeType":"VariableDeclaration","scope":96,"src":"994:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":41,"name":"uint256","nodeType":"ElementaryTypeName","src":"994:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":43,"length":{"hexValue":"33","id":42,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1002:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"994:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"components":[{"hexValue":"31","id":44,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1010:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},{"hexValue":"32","id":45,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1013:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},{"hexValue":"33","id":46,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1016:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"}],"id":47,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1009:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":53,"mutability":"mutable","name":"c","nameLocation":"1035:1:0","nodeType":"VariableDeclaration","scope":96,"src":"1024:16:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":49,"name":"uint256","nodeType":"ElementaryTypeName","src":"1024:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":51,"length":{"hexValue":"33","id":50,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1032:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"1024:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"id":52,"name":"a","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":40,"src":"1039:1:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3] storage ref"}},"visibility":"internal"},{"constant":false,"id":60,"mutability":"mutable","name":"d","nameLocation":"1057:1:0","nodeType":"VariableDeclaration","scope":96,"src":"1047:23:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":54,"name":"uint256","nodeType":"ElementaryTypeName","src":"1047:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":55,"nodeType":"ArrayTypeName","src":"1047:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"components":[{"hexValue":"34","id":56,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1062:1:0","typeDescriptions":{"typeIdentifier":"t_rational_4_by_1","typeString":"int_const 4"},"value":"4"},{"hexValue":"35","id":57,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1065:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},{"hexValue":"36","id":58,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1068:1:0","typeDescriptions":{"typeIdentifier":"t_rational_6_by_1","typeString":"int_const 6"},"value":"6"}],"id":59,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1061:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":67,"mutability":"mutable","name":"e","nameLocation":"1086:1:0","nodeType":"VariableDeclaration","scope":96,"src":"1076:23:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":61,"name":"uint256","nodeType":"ElementaryTypeName","src":"1076:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":62,"nodeType":"ArrayTypeName","src":"1076:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"components":[{"hexValue":"34","id":63,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1091:1:0","typeDescriptions":{"typeIdentifier":"t_rational_4_by_1","typeString":"int_const 4"},"value":"4"},{"hexValue":"35","id":64,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1094:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},{"hexValue":"36","id":65,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1097:1:0","typeDescriptions":{"typeIdentifier":"t_rational_6_by_1","typeString":"int_const 6"},"value":"6"}],"id":66,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1090:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":71,"mutability":"mutable","name":"f","nameLocation":"1115:1:0","nodeType":"VariableDeclaration","scope":96,"src":"1105:15:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":68,"name":"uint256","nodeType":"ElementaryTypeName","src":"1105:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":69,"nodeType":"ArrayTypeName","src":"1105:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"id":70,"name":"a","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":40,"src":"1119:1:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3] storage ref"}},"visibility":"internal"},{"constant":false,"id":77,"mutability":"mutable","name":"s","nameLocation":"1132:1:0","nodeType":"VariableDeclaration","scope":96,"src":"1127:16:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_struct$_Some_$29_storage","typeString":"struct EqEncoded.Some"},"typeName":{"id":73,"nodeType":"UserDefinedTypeName","pathNode":{"id":72,"name":"Some","nameLocations":["1127:4:0"],"nodeType":"IdentifierPath","referencedDeclaration":29,"src":"1127:4:0"},"referencedDeclaration":29,"src":"1127:4:0","typeDescriptions":{"typeIdentifier":"t_struct$_Some_$29_storage_ptr","typeString":"struct EqEncoded.Some"}},"value":{"arguments":[{"hexValue":"31","id":75,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1141:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"}],"expression":{"argumentTypes":[{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"}],"id":74,"name":"Some","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":29,"src":"1136:4:0","typeDescriptions":{"typeIdentifier":"t_type$_t_struct$_Some_$29_storage_ptr_$","typeString":"type(struct EqEncoded.Some storage pointer)"}},"id":76,"isConstant":false,"isLValue":false,"isPure":true,"kind":"structConstructorCall","lValueRequested":false,"nameLocations":[],"names":[],"nodeType":"FunctionCall","src":"1136:7:0","tryCall":false,"typeDescriptions":{"typeIdentifier":"t_struct$_Some_$29_memory_ptr","typeString":"struct EqEncoded.Some memory"}},"visibility":"internal"},{"body":{"id":85,"nodeType":"Block","src":"1818:28:0","statements":[{"expression":{"hexValue":"74727565","id":83,"isConstant":false,"isLValue":false,"isPure":true,"kind":"bool","lValueRequested":false,"nodeType":"Literal","src":"1835:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"value":"true"},"functionReturnParameters":82,"id":84,"nodeType":"Return","src":"1828:11:0"}]},"documentation":{"id":78,"nodeType":"StructuredDocumentation","src":"1150:621:0","text":"#if_succeeds eq_encoded(\"abc\", hex\"616263\");\n #if_succeeds eq_encoded(bytes2(0xffcc), bytes2(0xffcc));\n #if_succeeds eq_encoded(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n #if_succeeds eq_encoded(uint256(512), uint16(512));\n #if_succeeds eq_encoded(int256(-512), int256(-512));\n #if_succeeds eq_encoded(true, true);\n #if_succeeds eq_encoded(false, false);\n #if_succeeds eq_encoded(Some(1), s);\n #if_succeeds eq_encoded(Other.A, Other.A);\n #if_succeeds eq_encoded(a, b);\n #if_succeeds eq_encoded(d, e);"},"functionSelector":"d7d24afa","id":86,"implemented":true,"kind":"function","modifiers":[],"name":"positive","nameLocation":"1785:8:0","nodeType":"FunctionDefinition","parameters":{"id":79,"nodeType":"ParameterList","parameters":[],"src":"1793:2:0"},"returnParameters":{"id":82,"nodeType":"ParameterList","parameters":[{"constant":false,"id":81,"mutability":"mutable","name":"","nameLocation":"-1:-1:-1","nodeType":"VariableDeclaration","scope":86,"src":"1812:4:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"typeName":{"id":80,"name":"bool","nodeType":"ElementaryTypeName","src":"1812:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}},"visibility":"internal"}],"src":"1811:6:0"},"scope":96,"src":"1776:70:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"},{"body":{"id":94,"nodeType":"Block","src":"2589:28:0","statements":[{"expression":{"hexValue":"74727565","id":92,"isConstant":false,"isLValue":false,"isPure":true,"kind":"bool","lValueRequested":false,"nodeType":"Literal","src":"2606:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"value":"true"},"functionReturnParameters":91,"id":93,"nodeType":"Return","src":"2599:11:0"}]},"documentation":{"id":87,"nodeType":"StructuredDocumentation","src":"1852:690:0","text":"#if_succeeds !eq_encoded(\"abc\", \"abcd\");\n #if_succeeds !eq_encoded(\"abc\", \"def\");\n #if_succeeds !eq_encoded(hex\"616263\", hex\"616264\");\n #if_succeeds !eq_encoded(bytes2(0xffcc), bytes2(0xffff));\n #if_succeeds !eq_encoded(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n #if_succeeds !eq_encoded(uint256(512), uint16(1024));\n #if_succeeds !eq_encoded(int256(-512), int256(-1024));\n #if_succeeds !eq_encoded(true, false);\n #if_succeeds !eq_encoded(Some(2), s);\n #if_succeeds !eq_encoded(Other.A, Other.B);\n #if_succeeds !eq_encoded(a, d);\n #if_succeeds !eq_encoded(c, f);"},"functionSelector":"1cb3ef1f","id":95,"implemented":true,"kind":"function","modifiers":[],"name":"negative","nameLocation":"2556:8:0","nodeType":"FunctionDefinition","parameters":{"id":88,"nodeType":"ParameterList","parameters":[],"src":"2564:2:0"},"returnParameters":{"id":91,"nodeType":"ParameterList","parameters":[{"constant":false,"id":90,"mutability":"mutable","name":"","nameLocation":"-1:-1:-1","nodeType":"VariableDeclaration","scope":95,"src":"2583:4:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"typeName":{"id":89,"name":"bool","nodeType":"ElementaryTypeName","src":"2583:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}},"visibility":"internal"}],"src":"2582:6:0"},"scope":96,"src":"2547:70:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":97,"src":"861:1758:0","usedErrors":[],"usedEvents":[]}],"src":"65:2555:0","sourceEntryKey":"test/samples/predefined.sol"},"id":0,"source":"/// #const uint256 H := 60 * 60;\n/// #const uint256 D := H * 24;\ncontract A {\n /// #if_succeeds D == H * 24;\n function testHD() public {}\n}\n\n/// #const uint256 H := 60 * 60;\n/// #const uint256 D := H * 24;\n/// #const uint256 W := D * 7;\ncontract B {\n /// #if_succeeds W == D * 7 && D == H * 24 && H == 60 * 60;\n function testWHD() public {}\n}\n\ncontract C is B {\n /// #if_succeeds old(W) == D * 7;\n constructor() {}\n}\n\n// --------------------------------------------\n\n/// #define plus(uint x) uint = z + x;\n/// #define plus2(uint Foo) uint = z + Foo;\n/// #define plus3(uint plus2) uint = z + plus2;\n/// #define double(uint z) uint = z+z;\n/// #define quad(uint z) uint = let res := z+z in res + res;\n/// #define quad2(uint z) uint = double(double(z));\ncontract UserDefinedFunctions {\n\tuint z;\n}\n\n// --------------------------------------------\n\ncontract EqEncoded {\n struct Some {\n uint a;\n }\n\n enum Other {\n A, B\n }\n\n uint256[3] a = [1, 2, 3];\n uint256[3] b = [1, 2, 3];\n uint256[3] c = a;\n\n uint256[] d = [4, 5, 6];\n uint256[] e = [4, 5, 6];\n uint256[] f = a;\n\n Some s = Some(1);\n\n /// #if_succeeds eq_encoded(\"abc\", hex\"616263\");\n /// #if_succeeds eq_encoded(bytes2(0xffcc), bytes2(0xffcc));\n /// #if_succeeds eq_encoded(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n /// #if_succeeds eq_encoded(uint256(512), uint16(512));\n /// #if_succeeds eq_encoded(int256(-512), int256(-512));\n /// #if_succeeds eq_encoded(true, true);\n /// #if_succeeds eq_encoded(false, false);\n /// #if_succeeds eq_encoded(Some(1), s);\n /// #if_succeeds eq_encoded(Other.A, Other.A);\n /// #if_succeeds eq_encoded(a, b);\n /// #if_succeeds eq_encoded(d, e);\n function positive() public returns (bool) {\n return true;\n }\n\n /// #if_succeeds !eq_encoded(\"abc\", \"abcd\");\n /// #if_succeeds !eq_encoded(\"abc\", \"def\");\n /// #if_succeeds !eq_encoded(hex\"616263\", hex\"616264\");\n /// #if_succeeds !eq_encoded(bytes2(0xffcc), bytes2(0xffff));\n /// #if_succeeds !eq_encoded(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n /// #if_succeeds !eq_encoded(uint256(512), uint16(1024));\n /// #if_succeeds !eq_encoded(int256(-512), int256(-1024));\n /// #if_succeeds !eq_encoded(true, false);\n /// #if_succeeds !eq_encoded(Some(2), s);\n /// #if_succeeds !eq_encoded(Other.A, Other.B);\n /// #if_succeeds !eq_encoded(a, d);\n /// #if_succeeds !eq_encoded(c, f);\n function negative() public returns (bool) {\n return true;\n }\n}\n"}},"compilerVersion":"0.8.21"} \ No newline at end of file +{"sources":{"test/samples/predefined.sol":{"ast":{"absolutePath":"test/samples/predefined.sol","exportedSymbols":{"A":[8],"B":[15],"C":[23],"EqEncoded":[97],"UserDefinedFunctions":[27]},"id":98,"nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity","0.8",".20"],"nodeType":"PragmaDirective","src":"0:23:0"},{"abstract":false,"baseContracts":[],"canonicalName":"A","contractDependencies":[],"contractKind":"contract","documentation":{"id":2,"nodeType":"StructuredDocumentation","src":"24:65:0","text":"#const uint256 H := 60 * 60;\n #const uint256 D := H * 24;"},"fullyImplemented":true,"id":8,"linearizedBaseContracts":[8],"name":"A","nameLocation":"98:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":6,"nodeType":"Block","src":"165:2:0","statements":[]},"documentation":{"id":3,"nodeType":"StructuredDocumentation","src":"106:29:0","text":"#if_succeeds D == H * 24;"},"functionSelector":"540cffdc","id":7,"implemented":true,"kind":"function","modifiers":[],"name":"testHD","nameLocation":"149:6:0","nodeType":"FunctionDefinition","parameters":{"id":4,"nodeType":"ParameterList","parameters":[],"src":"155:2:0"},"returnParameters":{"id":5,"nodeType":"ParameterList","parameters":[],"src":"165:0:0"},"scope":8,"src":"140:27:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":98,"src":"89:80:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"B","contractDependencies":[],"contractKind":"contract","documentation":{"id":9,"nodeType":"StructuredDocumentation","src":"171:96:0","text":"#const uint256 H := 60 * 60;\n #const uint256 D := H * 24;\n #const uint256 W := D * 7;"},"fullyImplemented":true,"id":15,"linearizedBaseContracts":[15],"name":"B","nameLocation":"276:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":13,"nodeType":"Block","src":"374:2:0","statements":[]},"documentation":{"id":10,"nodeType":"StructuredDocumentation","src":"284:59:0","text":"#if_succeeds W == D * 7 && D == H * 24 && H == 60 * 60;"},"functionSelector":"3bf401bc","id":14,"implemented":true,"kind":"function","modifiers":[],"name":"testWHD","nameLocation":"357:7:0","nodeType":"FunctionDefinition","parameters":{"id":11,"nodeType":"ParameterList","parameters":[],"src":"364:2:0"},"returnParameters":{"id":12,"nodeType":"ParameterList","parameters":[],"src":"374:0:0"},"scope":15,"src":"348:28:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":98,"src":"267:111:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[{"baseName":{"id":16,"name":"B","nameLocations":["394:1:0"],"nodeType":"IdentifierPath","referencedDeclaration":15,"src":"394:1:0"},"id":17,"nodeType":"InheritanceSpecifier","src":"394:1:0"}],"canonicalName":"C","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":23,"linearizedBaseContracts":[23,15],"name":"C","nameLocation":"389:1:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":21,"nodeType":"Block","src":"454:2:0","statements":[]},"documentation":{"id":18,"nodeType":"StructuredDocumentation","src":"402:33:0","text":"#if_succeeds old(W) == D * 7;"},"id":22,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":19,"nodeType":"ParameterList","parameters":[],"src":"451:2:0"},"returnParameters":{"id":20,"nodeType":"ParameterList","parameters":[],"src":"454:0:0"},"scope":23,"src":"440:16:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":98,"src":"380:78:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"UserDefinedFunctions","contractDependencies":[],"contractKind":"contract","documentation":{"id":24,"nodeType":"StructuredDocumentation","src":"509:283:0","text":"#define plus(uint x) uint = z + x;\n #define plus2(uint Foo) uint = z + Foo;\n #define plus3(uint plus2) uint = z + plus2;\n #define double(uint z) uint = z+z;\n #define quad(uint z) uint = let res := z+z in res + res;\n #define quad2(uint z) uint = double(double(z));"},"fullyImplemented":true,"id":27,"linearizedBaseContracts":[27],"name":"UserDefinedFunctions","nameLocation":"801:20:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":26,"mutability":"mutable","name":"z","nameLocation":"830:1:0","nodeType":"VariableDeclaration","scope":27,"src":"825:6:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":25,"name":"uint","nodeType":"ElementaryTypeName","src":"825:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"scope":98,"src":"792:42:0","usedErrors":[],"usedEvents":[]},{"abstract":false,"baseContracts":[],"canonicalName":"EqEncoded","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":97,"linearizedBaseContracts":[97],"name":"EqEncoded","nameLocation":"894:9:0","nodeType":"ContractDefinition","nodes":[{"canonicalName":"EqEncoded.Some","id":30,"members":[{"constant":false,"id":29,"mutability":"mutable","name":"a","nameLocation":"937:1:0","nodeType":"VariableDeclaration","scope":30,"src":"932:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":28,"name":"uint","nodeType":"ElementaryTypeName","src":"932:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"name":"Some","nameLocation":"917:4:0","nodeType":"StructDefinition","scope":97,"src":"910:35:0","visibility":"public"},{"canonicalName":"EqEncoded.Other","id":33,"members":[{"id":31,"name":"A","nameLocation":"972:1:0","nodeType":"EnumValue","src":"972:1:0"},{"id":32,"name":"B","nameLocation":"975:1:0","nodeType":"EnumValue","src":"975:1:0"}],"name":"Other","nameLocation":"956:5:0","nodeType":"EnumDefinition","src":"951:31:0"},{"constant":false,"id":41,"mutability":"mutable","name":"a","nameLocation":"999:1:0","nodeType":"VariableDeclaration","scope":97,"src":"988:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":34,"name":"uint256","nodeType":"ElementaryTypeName","src":"988:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":36,"length":{"hexValue":"33","id":35,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"996:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"988:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"components":[{"hexValue":"31","id":37,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1004:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},{"hexValue":"32","id":38,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1007:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},{"hexValue":"33","id":39,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1010:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"}],"id":40,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1003:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":49,"mutability":"mutable","name":"b","nameLocation":"1029:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1018:24:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":42,"name":"uint256","nodeType":"ElementaryTypeName","src":"1018:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":44,"length":{"hexValue":"33","id":43,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1026:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"1018:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"components":[{"hexValue":"31","id":45,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1034:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},{"hexValue":"32","id":46,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1037:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},{"hexValue":"33","id":47,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1040:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"}],"id":48,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1033:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":54,"mutability":"mutable","name":"c","nameLocation":"1059:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1048:16:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3]"},"typeName":{"baseType":{"id":50,"name":"uint256","nodeType":"ElementaryTypeName","src":"1048:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":52,"length":{"hexValue":"33","id":51,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1056:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"ArrayTypeName","src":"1048:10:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage_ptr","typeString":"uint256[3]"}},"value":{"id":53,"name":"a","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":41,"src":"1063:1:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3] storage ref"}},"visibility":"internal"},{"constant":false,"id":61,"mutability":"mutable","name":"d","nameLocation":"1081:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1071:23:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":55,"name":"uint256","nodeType":"ElementaryTypeName","src":"1071:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":56,"nodeType":"ArrayTypeName","src":"1071:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"components":[{"hexValue":"34","id":57,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1086:1:0","typeDescriptions":{"typeIdentifier":"t_rational_4_by_1","typeString":"int_const 4"},"value":"4"},{"hexValue":"35","id":58,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1089:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},{"hexValue":"36","id":59,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1092:1:0","typeDescriptions":{"typeIdentifier":"t_rational_6_by_1","typeString":"int_const 6"},"value":"6"}],"id":60,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1085:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":68,"mutability":"mutable","name":"e","nameLocation":"1110:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1100:23:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":62,"name":"uint256","nodeType":"ElementaryTypeName","src":"1100:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":63,"nodeType":"ArrayTypeName","src":"1100:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"components":[{"hexValue":"34","id":64,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1115:1:0","typeDescriptions":{"typeIdentifier":"t_rational_4_by_1","typeString":"int_const 4"},"value":"4"},{"hexValue":"35","id":65,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1118:1:0","typeDescriptions":{"typeIdentifier":"t_rational_5_by_1","typeString":"int_const 5"},"value":"5"},{"hexValue":"36","id":66,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1121:1:0","typeDescriptions":{"typeIdentifier":"t_rational_6_by_1","typeString":"int_const 6"},"value":"6"}],"id":67,"isConstant":false,"isInlineArray":true,"isLValue":false,"isPure":true,"lValueRequested":false,"nodeType":"TupleExpression","src":"1114:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint8_$3_memory_ptr","typeString":"uint8[3] memory"}},"visibility":"internal"},{"constant":false,"id":72,"mutability":"mutable","name":"f","nameLocation":"1139:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1129:15:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage","typeString":"uint256[]"},"typeName":{"baseType":{"id":69,"name":"uint256","nodeType":"ElementaryTypeName","src":"1129:7:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":70,"nodeType":"ArrayTypeName","src":"1129:9:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$dyn_storage_ptr","typeString":"uint256[]"}},"value":{"id":71,"name":"a","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":41,"src":"1143:1:0","typeDescriptions":{"typeIdentifier":"t_array$_t_uint256_$3_storage","typeString":"uint256[3] storage ref"}},"visibility":"internal"},{"constant":false,"id":78,"mutability":"mutable","name":"s","nameLocation":"1156:1:0","nodeType":"VariableDeclaration","scope":97,"src":"1151:16:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_struct$_Some_$30_storage","typeString":"struct EqEncoded.Some"},"typeName":{"id":74,"nodeType":"UserDefinedTypeName","pathNode":{"id":73,"name":"Some","nameLocations":["1151:4:0"],"nodeType":"IdentifierPath","referencedDeclaration":30,"src":"1151:4:0"},"referencedDeclaration":30,"src":"1151:4:0","typeDescriptions":{"typeIdentifier":"t_struct$_Some_$30_storage_ptr","typeString":"struct EqEncoded.Some"}},"value":{"arguments":[{"hexValue":"31","id":76,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"1165:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"}],"expression":{"argumentTypes":[{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"}],"id":75,"name":"Some","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":30,"src":"1160:4:0","typeDescriptions":{"typeIdentifier":"t_type$_t_struct$_Some_$30_storage_ptr_$","typeString":"type(struct EqEncoded.Some storage pointer)"}},"id":77,"isConstant":false,"isLValue":false,"isPure":true,"kind":"structConstructorCall","lValueRequested":false,"nameLocations":[],"names":[],"nodeType":"FunctionCall","src":"1160:7:0","tryCall":false,"typeDescriptions":{"typeIdentifier":"t_struct$_Some_$30_memory_ptr","typeString":"struct EqEncoded.Some memory"}},"visibility":"internal"},{"body":{"id":86,"nodeType":"Block","src":"1842:28:0","statements":[{"expression":{"hexValue":"74727565","id":84,"isConstant":false,"isLValue":false,"isPure":true,"kind":"bool","lValueRequested":false,"nodeType":"Literal","src":"1859:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"value":"true"},"functionReturnParameters":83,"id":85,"nodeType":"Return","src":"1852:11:0"}]},"documentation":{"id":79,"nodeType":"StructuredDocumentation","src":"1174:621:0","text":"#if_succeeds eq_encoded(\"abc\", hex\"616263\");\n #if_succeeds eq_encoded(bytes2(0xffcc), bytes2(0xffcc));\n #if_succeeds eq_encoded(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n #if_succeeds eq_encoded(uint256(512), uint16(512));\n #if_succeeds eq_encoded(int256(-512), int256(-512));\n #if_succeeds eq_encoded(true, true);\n #if_succeeds eq_encoded(false, false);\n #if_succeeds eq_encoded(Some(1), s);\n #if_succeeds eq_encoded(Other.A, Other.A);\n #if_succeeds eq_encoded(a, b);\n #if_succeeds eq_encoded(d, e);"},"functionSelector":"d7d24afa","id":87,"implemented":true,"kind":"function","modifiers":[],"name":"positive","nameLocation":"1809:8:0","nodeType":"FunctionDefinition","parameters":{"id":80,"nodeType":"ParameterList","parameters":[],"src":"1817:2:0"},"returnParameters":{"id":83,"nodeType":"ParameterList","parameters":[{"constant":false,"id":82,"mutability":"mutable","name":"","nameLocation":"-1:-1:-1","nodeType":"VariableDeclaration","scope":87,"src":"1836:4:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"typeName":{"id":81,"name":"bool","nodeType":"ElementaryTypeName","src":"1836:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}},"visibility":"internal"}],"src":"1835:6:0"},"scope":97,"src":"1800:70:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"},{"body":{"id":95,"nodeType":"Block","src":"2613:28:0","statements":[{"expression":{"hexValue":"74727565","id":93,"isConstant":false,"isLValue":false,"isPure":true,"kind":"bool","lValueRequested":false,"nodeType":"Literal","src":"2630:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"value":"true"},"functionReturnParameters":92,"id":94,"nodeType":"Return","src":"2623:11:0"}]},"documentation":{"id":88,"nodeType":"StructuredDocumentation","src":"1876:690:0","text":"#if_succeeds !eq_encoded(\"abc\", \"abcd\");\n #if_succeeds !eq_encoded(\"abc\", \"def\");\n #if_succeeds !eq_encoded(hex\"616263\", hex\"616264\");\n #if_succeeds !eq_encoded(bytes2(0xffcc), bytes2(0xffff));\n #if_succeeds !eq_encoded(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n #if_succeeds !eq_encoded(uint256(512), uint16(1024));\n #if_succeeds !eq_encoded(int256(-512), int256(-1024));\n #if_succeeds !eq_encoded(true, false);\n #if_succeeds !eq_encoded(Some(2), s);\n #if_succeeds !eq_encoded(Other.A, Other.B);\n #if_succeeds !eq_encoded(a, d);\n #if_succeeds !eq_encoded(c, f);"},"functionSelector":"1cb3ef1f","id":96,"implemented":true,"kind":"function","modifiers":[],"name":"negative","nameLocation":"2580:8:0","nodeType":"FunctionDefinition","parameters":{"id":89,"nodeType":"ParameterList","parameters":[],"src":"2588:2:0"},"returnParameters":{"id":92,"nodeType":"ParameterList","parameters":[{"constant":false,"id":91,"mutability":"mutable","name":"","nameLocation":"-1:-1:-1","nodeType":"VariableDeclaration","scope":96,"src":"2607:4:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"},"typeName":{"id":90,"name":"bool","nodeType":"ElementaryTypeName","src":"2607:4:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}},"visibility":"internal"}],"src":"2606:6:0"},"scope":97,"src":"2571:70:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":98,"src":"885:1758:0","usedErrors":[],"usedEvents":[]}],"src":"0:2644:0","sourceEntryKey":"test/samples/predefined.sol"},"id":0,"source":"pragma solidity 0.8.20;\n/// #const uint256 H := 60 * 60;\n/// #const uint256 D := H * 24;\ncontract A {\n /// #if_succeeds D == H * 24;\n function testHD() public {}\n}\n\n/// #const uint256 H := 60 * 60;\n/// #const uint256 D := H * 24;\n/// #const uint256 W := D * 7;\ncontract B {\n /// #if_succeeds W == D * 7 && D == H * 24 && H == 60 * 60;\n function testWHD() public {}\n}\n\ncontract C is B {\n /// #if_succeeds old(W) == D * 7;\n constructor() {}\n}\n\n// --------------------------------------------\n\n/// #define plus(uint x) uint = z + x;\n/// #define plus2(uint Foo) uint = z + Foo;\n/// #define plus3(uint plus2) uint = z + plus2;\n/// #define double(uint z) uint = z+z;\n/// #define quad(uint z) uint = let res := z+z in res + res;\n/// #define quad2(uint z) uint = double(double(z));\ncontract UserDefinedFunctions {\n\tuint z;\n}\n\n// --------------------------------------------\n\ncontract EqEncoded {\n struct Some {\n uint a;\n }\n\n enum Other {\n A, B\n }\n\n uint256[3] a = [1, 2, 3];\n uint256[3] b = [1, 2, 3];\n uint256[3] c = a;\n\n uint256[] d = [4, 5, 6];\n uint256[] e = [4, 5, 6];\n uint256[] f = a;\n\n Some s = Some(1);\n\n /// #if_succeeds eq_encoded(\"abc\", hex\"616263\");\n /// #if_succeeds eq_encoded(bytes2(0xffcc), bytes2(0xffcc));\n /// #if_succeeds eq_encoded(0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n /// #if_succeeds eq_encoded(uint256(512), uint16(512));\n /// #if_succeeds eq_encoded(int256(-512), int256(-512));\n /// #if_succeeds eq_encoded(true, true);\n /// #if_succeeds eq_encoded(false, false);\n /// #if_succeeds eq_encoded(Some(1), s);\n /// #if_succeeds eq_encoded(Other.A, Other.A);\n /// #if_succeeds eq_encoded(a, b);\n /// #if_succeeds eq_encoded(d, e);\n function positive() public returns (bool) {\n return true;\n }\n\n /// #if_succeeds !eq_encoded(\"abc\", \"abcd\");\n /// #if_succeeds !eq_encoded(\"abc\", \"def\");\n /// #if_succeeds !eq_encoded(hex\"616263\", hex\"616264\");\n /// #if_succeeds !eq_encoded(bytes2(0xffcc), bytes2(0xffff));\n /// #if_succeeds !eq_encoded(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF, 0xC0FfEec0ffeeC0FfEec0fFEec0FfeEc0fFEe0000);\n /// #if_succeeds !eq_encoded(uint256(512), uint16(1024));\n /// #if_succeeds !eq_encoded(int256(-512), int256(-1024));\n /// #if_succeeds !eq_encoded(true, false);\n /// #if_succeeds !eq_encoded(Some(2), s);\n /// #if_succeeds !eq_encoded(Other.A, Other.B);\n /// #if_succeeds !eq_encoded(a, d);\n /// #if_succeeds !eq_encoded(c, f);\n function negative() public returns (bool) {\n return true;\n }\n}\n"}},"compilerVersion":"0.8.20"} \ No newline at end of file diff --git a/test/samples/skip_invariant_double_check.instrumented.sol b/test/samples/skip_invariant_double_check.instrumented.sol index 71d13b43..1a8021c0 100644 --- a/test/samples/skip_invariant_double_check.instrumented.sol +++ b/test/samples/skip_invariant_double_check.instrumented.sol @@ -1,6 +1,6 @@ /// This file is auto-generated by Scribble and shouldn't be edited directly. /// Use --disarm prior to make any changes. -pragma solidity 0.8.21; +pragma solidity 0.8.20; /// #invariant true; contract Foo { @@ -11,23 +11,23 @@ contract Foo { /// #if_succeeds false; constructor(uint x) { vars1 memory _v; - _v.__scribble_check_invs_at_end = !__ScribbleUtilsLib__10.isInContract(); - __ScribbleUtilsLib__10.setInContract(true); + _v.__scribble_check_invs_at_end = !__ScribbleUtilsLib__11.isInContract(); + __ScribbleUtilsLib__11.setInContract(true); unchecked { if (!(false)) { - emit __ScribbleUtilsLib__10.AssertionFailed("000529:0066:000 1: "); + emit __ScribbleUtilsLib__11.AssertionFailed("000529:0066:000 1: "); assert(false); } } if (_v.__scribble_check_invs_at_end) __scribble_check_state_invariants(); - __ScribbleUtilsLib__10.setInContract(!_v.__scribble_check_invs_at_end); + __ScribbleUtilsLib__11.setInContract(!_v.__scribble_check_invs_at_end); } /// Check only the current contract's state invariants function __scribble_Foo_check_state_invariants_internal() internal { unchecked { if (!(true)) { - emit __ScribbleUtilsLib__10.AssertionFailed("001016:0066:000 0: "); + emit __ScribbleUtilsLib__11.AssertionFailed("001016:0066:000 0: "); assert(false); } } @@ -39,7 +39,7 @@ contract Foo { } } -library __ScribbleUtilsLib__10 { +library __ScribbleUtilsLib__11 { event AssertionFailed(string message); event AssertionFailedData(int eventId, bytes encodingData); diff --git a/test/samples/skip_invariant_double_check.sol b/test/samples/skip_invariant_double_check.sol index 5252df7a..c9e801ce 100644 --- a/test/samples/skip_invariant_double_check.sol +++ b/test/samples/skip_invariant_double_check.sol @@ -1,3 +1,4 @@ +pragma solidity 0.8.20; /** * The original constructor in this sample * SHOULD NOT be instrumented. diff --git a/test/samples/skip_invariant_double_check.sol.json b/test/samples/skip_invariant_double_check.sol.json index 57272ca2..cf6b2181 100644 --- a/test/samples/skip_invariant_double_check.sol.json +++ b/test/samples/skip_invariant_double_check.sol.json @@ -1 +1 @@ -{"sources":{"test/samples/skip_invariant_double_check.sol":{"ast":{"absolutePath":"test/samples/skip_invariant_double_check.sol","exportedSymbols":{"Foo":[9]},"id":10,"nodeType":"SourceUnit","nodes":[{"abstract":false,"baseContracts":[],"canonicalName":"Foo","contractDependencies":[],"contractKind":"contract","documentation":{"id":1,"nodeType":"StructuredDocumentation","src":"142:21:0","text":"#invariant true;"},"fullyImplemented":true,"id":9,"linearizedBaseContracts":[9],"name":"Foo","nameLocation":"172:3:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":7,"nodeType":"Block","src":"238:2:0","statements":[]},"documentation":{"id":2,"nodeType":"StructuredDocumentation","src":"183:23:0","text":"#if_succeeds false;"},"id":8,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":5,"nodeType":"ParameterList","parameters":[{"constant":false,"id":4,"mutability":"mutable","name":"x","nameLocation":"228:1:0","nodeType":"VariableDeclaration","scope":8,"src":"223:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":3,"name":"uint","nodeType":"ElementaryTypeName","src":"223:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"src":"222:8:0"},"returnParameters":{"id":6,"nodeType":"ParameterList","parameters":[],"src":"238:0:0"},"scope":9,"src":"211:29:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":10,"src":"163:79:0","usedErrors":[],"usedEvents":[]}],"src":"163:80:0","sourceEntryKey":"test/samples/skip_invariant_double_check.sol"},"id":0,"source":"/**\n * The original constructor in this sample\n * SHOULD NOT be instrumented.\n *\n * See https://github.com/ConsenSys/scribble/issues/140\n */\n\n/// #invariant true;\ncontract Foo {\n\n /// #if_succeeds false;\n constructor(uint x) public {}\n}\n"}},"compilerVersion":"0.8.21"} \ No newline at end of file +{"sources":{"test/samples/skip_invariant_double_check.sol":{"ast":{"absolutePath":"test/samples/skip_invariant_double_check.sol","exportedSymbols":{"Foo":[10]},"id":11,"nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity","0.8",".20"],"nodeType":"PragmaDirective","src":"0:23:0"},{"abstract":false,"baseContracts":[],"canonicalName":"Foo","contractDependencies":[],"contractKind":"contract","documentation":{"id":2,"nodeType":"StructuredDocumentation","src":"166:21:0","text":"#invariant true;"},"fullyImplemented":true,"id":10,"linearizedBaseContracts":[10],"name":"Foo","nameLocation":"196:3:0","nodeType":"ContractDefinition","nodes":[{"body":{"id":8,"nodeType":"Block","src":"262:2:0","statements":[]},"documentation":{"id":3,"nodeType":"StructuredDocumentation","src":"207:23:0","text":"#if_succeeds false;"},"id":9,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":6,"nodeType":"ParameterList","parameters":[{"constant":false,"id":5,"mutability":"mutable","name":"x","nameLocation":"252:1:0","nodeType":"VariableDeclaration","scope":9,"src":"247:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":4,"name":"uint","nodeType":"ElementaryTypeName","src":"247:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"src":"246:8:0"},"returnParameters":{"id":7,"nodeType":"ParameterList","parameters":[],"src":"262:0:0"},"scope":10,"src":"235:29:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":11,"src":"187:79:0","usedErrors":[],"usedEvents":[]}],"src":"0:267:0","sourceEntryKey":"test/samples/skip_invariant_double_check.sol"},"id":0,"source":"pragma solidity 0.8.20;\n/**\n * The original constructor in this sample\n * SHOULD NOT be instrumented.\n *\n * See https://github.com/ConsenSys/scribble/issues/140\n */\n\n/// #invariant true;\ncontract Foo {\n\n /// #if_succeeds false;\n constructor(uint x) public {}\n}\n"}},"compilerVersion":"0.8.20"} \ No newline at end of file