diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json index e69de29b..39376114 100644 --- a/tests/frontend/pass/token/transfer.act.typed.json +++ b/tests/frontend/pass/token/transfer.act.typed.json @@ -0,0 +1,6433 @@ +{ + "contracts": [ + { + "behaviours": [ + { + "case": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "=/=" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transfer", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [ + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "-" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "+" + } + } + ] + }, + { + "case": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transfer", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "value" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [] + }, + { + "case": [ + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "type": "Address" + }, + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transferFrom", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [ + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + } + } + ] + }, + { + "case": [ + { + "args": [ + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "args": [ + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + }, + { + "literal": "1", + "type": "int" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "type": "Address" + }, + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transferFrom", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [ + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + } + } + ] + }, + { + "case": [ + { + "args": [ + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "args": [ + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + }, + { + "literal": "1", + "type": "int" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "type": "Address" + }, + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transferFrom", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [ + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + } + } + ] + }, + { + "case": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "contract": "Token", + "interface": { + "args": [ + { + "abitype": { + "type": "Address" + }, + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "Address" + }, + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transferFrom", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "+" + }, + { + "args": [ + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } + ], + "arity": 2, + "symbol": "^" + } + ], + "arity": 2, + "symbol": "<" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "=/=" + }, + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "-" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "=>" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "0", + "type": "int" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "amount" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "abitype": { + "type": "Address" + }, + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Callvalue", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Callvalue", + "type": "int" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "returns": { + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + }, + "stateUpdates": [] + } + ], + "constructor": { + "contract": "Token", + "initialStorage": [ + { + "location": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "name" + }, + "type": "bytestring" + }, + "value": { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_name" + } + }, + { + "location": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "symbol" + }, + "type": "bytestring" + }, + "value": { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_symbol" + } + }, + { + "location": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "value": { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + }, + { + "location": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "value": { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + } + ], + "interface": { + "args": [ + { + "abitype": { + "type": "String" + }, + "id": "\"_symbol\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "String" + }, + "id": "\"_name\"", + "kind": "Declaration" + }, + { + "abitype": { + "type": "String" + }, + "id": "\"_version\"", + "kind": "Declaration" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "id": "\"_totalSupply\"", + "kind": "Declaration" + } + ], + "id": "\"Token\"", + "kind": "Interface" + }, + "invariants": [ + { + "contract": "Token", + "kind": "Invariant", + "preconditions": [ + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "predicate": [ + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Post" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "storagebounds": [ + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ] + }, + { + "contract": "Token", + "kind": "Invariant", + "preconditions": [ + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "predicate": [ + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "name" + }, + "type": "bytestring" + }, + "timing": "Pre" + }, + { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_name" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "name" + }, + "type": "bytestring" + }, + "timing": "Post" + }, + { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_name" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "storagebounds": [] + }, + { + "contract": "Token", + "kind": "Invariant", + "preconditions": [ + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ], + "predicate": [ + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "symbol" + }, + "type": "bytestring" + }, + "timing": "Pre" + }, + { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_symbol" + } + ], + "arity": 2, + "symbol": "==" + }, + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "symbol" + }, + "type": "bytestring" + }, + "timing": "Post" + }, + { + "abitype": { + "type": "String" + }, + "type": "bytestring", + "var": "_symbol" + } + ], + "arity": 2, + "symbol": "==" + } + ], + "storagebounds": [] + } + ], + "kind": "Constructor", + "postConditions": [], + "preConditions": [ + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "abitype": { + "size": "256", + "type": "UInt" + }, + "type": "int", + "var": "_totalSupply" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "entry": { + "item": { + "indexes": [ + { + "expression": { + "ethEnv": "Caller", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" + } + ], + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } + }, + "type": "int" + }, + "timing": "Pre" + }, + { + "literal": "115792089237316195423570985008687907853269984665640564039457584007913129639935", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + }, + { + "args": [ + { + "args": [ + { + "literal": "0", + "type": "int" + }, + { + "ethEnv": "Caller", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + }, + { + "args": [ + { + "ethEnv": "Caller", + "type": "int" + }, + { + "literal": "1461501637330902918203684832716283019655932542975", + "type": "int" + } + ], + "arity": 2, + "symbol": "<=" + } + ], + "arity": 2, + "symbol": "and" + } + ] + }, + "kind": "Contract" + } + ], + "kind": "Act", + "store": { + "kind": "Storages", + "storages": { + "Token": { + "allowance": [ + { + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + }, + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } + }, + 4 + ], + "balanceOf": [ + { + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } + }, + 3 + ], + "name": [ + { + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } + }, + 0 + ], + "symbol": [ + { + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } + }, + 1 + ], + "totalSupply": [ + { + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } + }, + 2 + ] + } + } + } +}