diff --git a/src/Syntax/TimeAgnostic.hs b/src/Syntax/TimeAgnostic.hs index 0f974e7e..5f7d89bf 100644 --- a/src/Syntax/TimeAgnostic.hs +++ b/src/Syntax/TimeAgnostic.hs @@ -352,24 +352,24 @@ instance Timable StorageRef where -- It was difficult to construct a function with type: -- `InvPredicate t -> Either (Exp Bool Timed,Exp Bool Timed) (Exp Bool Untimed)` instance ToJSON (Act Timed) where - toJSON (Act storages contracts) = object [ "kind" .= String "Program" + toJSON (Act storages contracts) = object [ "kind" .= String "Act" , "store" .= storeJSON storages , "contracts" .= toJSON contracts ] instance ToJSON (Act Untimed) where - toJSON (Act storages contracts) = object [ "kind" .= String "Program" + toJSON (Act storages contracts) = object [ "kind" .= String "Act" , "store" .= storeJSON storages , "contracts" .= toJSON contracts ] instance ToJSON (Contract Timed) where toJSON (Contract ctor behv) = object [ "kind" .= String "Contract" - , "constructor" .= toJSON ctor - , "behaviors" .= toJSON behv ] + , "constructor" .= toJSON ctor + , "behaviours" .= toJSON behv ] instance ToJSON (Contract Untimed) where toJSON (Contract ctor behv) = object [ "kind" .= String "Contract" - , "constructor" .= toJSON ctor - , "behaviors" .= toJSON behv ] + , "constructor" .= toJSON ctor + , "behaviours" .= toJSON behv ] storeJSON :: Store -> Value @@ -379,7 +379,7 @@ storeJSON storages = object [ "kind" .= String "Storages" instance ToJSON (Constructor Timed) where toJSON Constructor{..} = object [ "kind" .= String "Constructor" , "contract" .= _cname - , "interface" .= (String . pack $ show _cinterface) + , "interface" .= toJSON _cinterface , "preConditions" .= toJSON _cpreconditions , "postConditions" .= toJSON _cpostconditions , "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants @@ -388,7 +388,7 @@ instance ToJSON (Constructor Timed) where instance ToJSON (Constructor Untimed) where toJSON Constructor{..} = object [ "kind" .= String "Constructor" , "contract" .= _cname - , "interface" .= (String . pack $ show _cinterface) + , "interface" .= toJSON _cinterface , "preConditions" .= toJSON _cpreconditions , "postConditions" .= toJSON _cpostconditions , "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants @@ -398,13 +398,26 @@ instance ToJSON (Behaviour t) where toJSON Behaviour{..} = object [ "kind" .= String "Behaviour" , "name" .= _name , "contract" .= _contract - , "interface" .= (String . pack $ show _interface) + , "interface" .= toJSON _interface , "preConditions" .= toJSON _preconditions , "case" .= toJSON _caseconditions , "postConditions" .= toJSON _postconditions , "stateUpdates" .= toJSON _stateUpdates , "returns" .= toJSON _returns ] +instance ToJSON Interface where + toJSON (Interface x decls) = object [ "kind" .= String "Interface" + , "id" .= pack (show x) + , "args" .= toJSON decls + ] + +instance ToJSON Decl where + toJSON (Decl abitype x) = object [ "kind" .= String "Declaration" + , "id" .= pack (show x) + , "abitype" .= pack (show abitype) + ] + + invariantJSON :: ToJSON pred => Invariant t -> pred -> Value invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant" , "predicate" .= toJSON predicate @@ -413,8 +426,8 @@ invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant" , "contract" .= _icontract ] instance ToJSON (Rewrite t) where - toJSON (Constant a) = object [ "Constant" .= toJSON a ] - toJSON (Rewrite a) = object [ "Rewrite" .= toJSON a ] + toJSON (Constant a) = object [ "constant" .= toJSON a ] + toJSON (Rewrite a) = object [ "rewrite" .= toJSON a ] instance ToJSON (StorageLocation t) where toJSON (Loc _ a) = object [ "location" .= toJSON a ] @@ -423,26 +436,33 @@ instance ToJSON (StorageUpdate t) where toJSON (Update _ a b) = object [ "location" .= toJSON a ,"value" .= toJSON b ] instance ToJSON (TStorageItem a t) where - toJSON (Item t _ a) = object [ "sort" .= pack (show t) - , "item" .= toJSON a ] + toJSON (Item t _ a) = object [ "item" .= toJSON a + , "type" .= show t + ] instance ToJSON (StorageRef t) where - toJSON (SVar _ c x) = object [ "var" .= String (pack c <> "." <> pack x) ] + toJSON (SVar _ c x) = object [ "kind" .= pack "SVar" + , "svar" .= pack x + , "contract" .= pack c ] toJSON (SMapping _ e xs) = mapping e xs - toJSON (SField _ e _ x) = field e x + toJSON (SField _ e c x) = field e c x mapping :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value -mapping a b = object [ "symbol" .= pack "lookup" - , "arity" .= Data.Aeson.Types.Number 2 - , "args" .= Array (fromList [toJSON a, toJSON b]) ] +mapping a b = object [ "kind" .= pack "Mapping" + , "indexes" .= toJSON b + , "reference" .= toJSON a] + +field :: (ToJSON a1) => a1 -> Id -> Id -> Value +field a c x = object [ "kind" .= pack "Field" + , "field" .= pack x + , "contract" .= pack c + , "reference" .= toJSON a + ] -field :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value -field a b = object [ "symbol" .= pack "select" - , "arity" .= Data.Aeson.Types.Number 2 - , "args" .= Array (fromList [toJSON a, toJSON b]) ] instance ToJSON (TypedExp t) where - toJSON (TExp typ a) = object [ "sort" .= pack (show typ) + toJSON (TExp typ a) = object [ "kind" .= pack "TypedExpr" + , "type" .= pack (show typ) , "expression" .= toJSON a ] instance ToJSON (Exp a t) where @@ -451,14 +471,15 @@ instance ToJSON (Exp a t) where toJSON (Exp _ a b) = symbol "^" a b toJSON (Mul _ a b) = symbol "*" a b toJSON (Div _ a b) = symbol "/" a b - toJSON (LitInt _ a) = toJSON $ show a + toJSON (LitInt _ a) = object [ "literal" .= pack (show a) + , "type" .= pack "int" ] toJSON (IntMin _ a) = toJSON $ show $ intmin a toJSON (IntMax _ a) = toJSON $ show $ intmax a toJSON (UIntMin _ a) = toJSON $ show $ uintmin a toJSON (UIntMax _ a) = toJSON $ show $ uintmax a - toJSON (InRange _ a b) = object [ "symbol" .= pack ("inrange" <> show a) - , "arity" .= Data.Aeson.Types.Number 1 - , "args" .= Array (fromList [toJSON b]) ] + toJSON (InRange _ a b) = object [ "symbol" .= pack "inrange" + , "arity" .= Data.Aeson.Types.Number 2 + , "args" .= Array (fromList [String (pack $ show a), toJSON b]) ] toJSON (IntEnv _ a) = String $ pack $ show a toJSON (ITE _ a b c) = object [ "symbol" .= pack "ite" , "arity" .= Data.Aeson.Types.Number 3 @@ -472,7 +493,8 @@ instance ToJSON (Exp a t) where toJSON (Eq _ _ a b) = symbol "==" a b toJSON (LEQ _ a b) = symbol "<=" a b toJSON (GEQ _ a b) = symbol ">=" a b - toJSON (LitBool _ a) = String $ pack $ show a + toJSON (LitBool _ a) = object [ "literal" .= pack (show a) + , "type" .= pack "bool" ] toJSON (Neg _ a) = object [ "symbol" .= pack "not" , "arity" .= Data.Aeson.Types.Number 1 , "args" .= Array (fromList [toJSON a]) ] @@ -481,18 +503,24 @@ instance ToJSON (Exp a t) where toJSON (Slice _ s a b) = object [ "symbol" .= pack "slice" , "arity" .= Data.Aeson.Types.Number 3 , "args" .= Array (fromList [toJSON s, toJSON a, toJSON b]) ] - toJSON (ByStr _ a) = toJSON a - toJSON (ByLit _ a) = String . pack $ show a - toJSON (ByEnv _ a) = String . pack $ show a - - toJSON (TEntry _ t a) = object [ fromString (show t) .= toJSON a ] - toJSON (Var _ _ _ a) = toJSON a + toJSON (ByStr _ a) = object [ "bytestring" .= toJSON a + , "type" .= pack "bool" ] + toJSON (ByLit _ a) = object [ "literal" .= pack (show a) + , "type" .= pack "bytestring" ] + toJSON (ByEnv _ a) = object [ "ethEnv" .= pack (show a) + , "type" .= pack "bytestring" ] + toJSON (TEntry _ t a) = object [ "entry" .= toJSON a + , "timing" .= show t ] + toJSON (Var _ t _ a) = object [ "var" .= toJSON a + , "type" .= show t ] toJSON (Create _ f xs) = object [ "symbol" .= pack "create" - , "arity" .= Data.Aeson.Types.Number 2 - , "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ] + , "arity" .= Data.Aeson.Types.Number 2 + , "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ] toJSON v = error $ "todo: json ast for: " <> show v + + symbol :: (ToJSON a1, ToJSON a2) => String -> a1 -> a2 -> Value symbol s a b = object [ "symbol" .= pack s , "arity" .= Data.Aeson.Types.Number 2 diff --git a/src/Syntax/Untyped.hs b/src/Syntax/Untyped.hs index 1b10feee..9c15bd45 100644 --- a/src/Syntax/Untyped.hs +++ b/src/Syntax/Untyped.hs @@ -7,9 +7,10 @@ module Syntax.Untyped (module Syntax.Untyped) where import Data.Aeson import Data.List (intercalate) -import Data.List.NonEmpty (toList, NonEmpty) +import Data.List.NonEmpty (NonEmpty) +import Data.Text as T (pack) -import EVM.ABI (AbiType) +import EVM.ABI (AbiType(..)) import Lex type Pn = AlexPosn @@ -154,6 +155,7 @@ instance Show SlotType where <> ")") (show t) s + data StorageVar = StorageVar Pn SlotType Id deriving (Eq, Show) @@ -164,10 +166,41 @@ instance Show Decl where show (Decl t a) = show t <> " " <> a instance ToJSON SlotType where - toJSON (StorageValue t) = object ["type" .= show t] - toJSON (StorageMapping ixTypes valType) = object [ "type" .= String "mapping" - , "ixTypes" .= show (toList ixTypes) - , "valType" .= show valType] + toJSON (StorageValue t) = object ["kind" .= String "ValueType" + , "valueType" .= toJSON t] + toJSON (StorageMapping ixTypes resType) = object [ "kind" .= String "MappingType" + , "ixTypes" .= toJSON ixTypes + , "resType" .= toJSON resType] + + +instance ToJSON ValueType where + toJSON (ContractType c) = object [ "kind" .= String "ContractType" + , "name" .= show c ] + toJSON (PrimitiveType abiType) = object [ "kind" .= String "AbiType" + , "abiType" .= toJSON abiType ] + + +instance ToJSON AbiType where + toJSON (AbiUIntType n) = object [ "type" .= String "UInt" + , "size" .= String (T.pack $ show n) ] + toJSON (AbiIntType n) = object [ "type" .= String "Int" + , "size" .= String (T.pack $ show n) ] + toJSON AbiAddressType = object [ "type" .= String "Address" ] + toJSON AbiBoolType = object [ "type" .= String "Bool" ] + toJSON (AbiBytesType n) = object [ "type" .= String "Bytes" + , "size" .= String (T.pack $ show n) ] + toJSON AbiBytesDynamicType = object [ "type" .= String "BytesDynamic" ] + toJSON AbiStringType = object [ "type" .= String "String" ] + toJSON (AbiArrayDynamicType t) = object [ "type" .= String "ArrayDynamic" + , "arrayType" .= toJSON t ] + toJSON (AbiArrayType n t) = object [ "type" .= String "Array" + , "arrayType" .= toJSON t + , "size" .= String (T.pack $ show n) ] + toJSON (AbiTupleType ts) = object [ "type" .= String "Tuple" + , "elemTypes" .= toJSON ts ] + toJSON (AbiFunctionType) = object [ "type" .= String "Function" ] + + -- Create the string that is used to construct the function selector makeIface :: Interface -> String diff --git a/tests/frontend/pass/case/case.act.typed.json b/tests/frontend/pass/case/case.act.typed.json index bf8909fc..0de11f7a 100644 --- a/tests/frontend/pass/case/case.act.typed.json +++ b/tests/frontend/pass/case/case.act.typed.json @@ -1,20 +1,36 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ { "args": [ - "z", - "0" + { + "type": "int", + "var": "z" + }, + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -22,7 +38,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -31,15 +50,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -53,14 +81,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -69,12 +103,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -89,7 +126,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -111,14 +151,19 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] @@ -127,15 +172,31 @@ "case": [ { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "==" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -143,7 +204,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -152,15 +216,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -174,14 +247,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -190,12 +269,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -210,7 +292,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -232,17 +317,25 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, "value": { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "+" @@ -255,15 +348,31 @@ "case": [ { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": ">" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -271,7 +380,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -280,15 +392,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -302,14 +423,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -318,12 +445,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -338,7 +468,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -360,17 +493,25 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, "value": { "args": [ - "z", - "2" + { + "type": "int", + "var": "z" + }, + { + "literal": "2", + "type": "int" + } ], "arity": 2, "symbol": "+" @@ -386,14 +527,23 @@ { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } } ], - "interface": "C()", + "interface": { + "args": [], + "id": "\"C\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -402,14 +552,21 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { "C": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] diff --git a/tests/frontend/pass/creation/create.act.typed.json b/tests/frontend/pass/creation/create.act.typed.json index 240692e8..27902efa 100644 --- a/tests/frontend/pass/creation/create.act.typed.json +++ b/tests/frontend/pass/creation/create.act.typed.json @@ -1,30 +1,41 @@ { "contracts": [ { - "behaviors": [], + "behaviours": [], "constructor": { "contract": "Modest", "initial storage": [ { "location": { "item": { - "var": "Modest.x" + "contract": "Modest", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "1" + "value": { + "literal": "1", + "type": "int" + } }, { "location": { "item": { - "var": "Modest.y" + "contract": "Modest", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, "value": "Caller" } ], - "interface": "Modest()", + "interface": { + "args": [], + "id": "\"Modest\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -33,7 +44,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -56,20 +70,33 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { "Modest": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ], "y": [ { - "type": "address" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } }, 1 ] diff --git a/tests/frontend/pass/multi/multi.act.typed.json b/tests/frontend/pass/multi/multi.act.typed.json index c8ceeaed..e1ae9788 100644 --- a/tests/frontend/pass/multi/multi.act.typed.json +++ b/tests/frontend/pass/multi/multi.act.typed.json @@ -1,21 +1,30 @@ { "contracts": [ { - "behaviors": [], + "behaviours": [], "constructor": { "contract": "A", "initial storage": [ { "location": { "item": { - "var": "A.x" + "contract": "A", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } } ], - "interface": "A()", + "interface": { + "args": [], + "id": "\"A\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -24,13 +33,26 @@ "kind": "Contract" }, { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "B", - "interface": "set_remote(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"set_remote\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "remote", "postConditions": [], @@ -38,7 +60,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -47,15 +72,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -69,21 +103,25 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -92,19 +130,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -119,7 +158,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -141,31 +183,47 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] }, { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "B", - "interface": "set_remote2(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"set_remote2\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "multi", "postConditions": [], @@ -173,7 +231,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -182,15 +243,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -204,14 +274,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -220,12 +296,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -240,21 +319,25 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -263,19 +346,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -290,7 +374,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -312,32 +399,40 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, - "value": "1" + "value": { + "literal": "1", + "type": "int" + } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] @@ -349,18 +444,25 @@ { "location": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } }, { "location": { "item": { - "var": "B.a" + "contract": "B", + "kind": "SVar", + "svar": "a" }, - "sort": "contract" + "type": "contract" }, "value": { "args": [ @@ -374,7 +476,11 @@ } } ], - "interface": "B()", + "interface": { + "args": [], + "id": "\"B\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -383,14 +489,21 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { "A": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] @@ -398,13 +511,24 @@ "B": { "a": [ { - "type": "A" + "kind": "ValueType", + "valueType": { + "kind": "ContractType", + "name": "\"A\"" + } }, 1 ], "y": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] diff --git a/tests/frontend/pass/safemath/safemathraw.act.typed.json b/tests/frontend/pass/safemath/safemathraw.act.typed.json index ae223cda..97bdcb4b 100644 --- a/tests/frontend/pass/safemath/safemathraw.act.typed.json +++ b/tests/frontend/pass/safemath/safemathraw.act.typed.json @@ -1,49 +1,85 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "SafeAdd", - "interface": "add(uint256 x, uint256 y)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"x\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"y\"", + "kind": "Declaration" + } + ], + "id": "\"add\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "add", "postConditions": [], "preConditions": [ { "args": [ + "uint256", { "args": [ - "x", - "y" + { + "type": "int", + "var": "x" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "+" } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ - "x" + "uint256", + { + "type": "int", + "var": "x" + } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ - "y" + "uint256", + { + "type": "int", + "var": "y" + } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -52,15 +88,24 @@ "args": [ { "args": [ - "0", - "x" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "x" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "x", + { + "type": "int", + "var": "x" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -74,15 +119,24 @@ "args": [ { "args": [ - "0", - "y" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "y", + { + "type": "int", + "var": "y" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -96,7 +150,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -118,13 +175,20 @@ "returns": { "expression": { "args": [ - "x", - "y" + { + "type": "int", + "var": "x" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "+" }, - "sort": "int" + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [] } @@ -132,7 +196,11 @@ "constructor": { "contract": "SafeAdd", "initial storage": [], - "interface": "SafeAdd()", + "interface": { + "args": [], + "id": "\"SafeAdd\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -141,7 +209,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/smoke/smoke.act.typed.json b/tests/frontend/pass/smoke/smoke.act.typed.json index d3dbbf40..bf4aaad5 100644 --- a/tests/frontend/pass/smoke/smoke.act.typed.json +++ b/tests/frontend/pass/smoke/smoke.act.typed.json @@ -1,13 +1,26 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "A", - "interface": "f(uint256 x)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"x\"", + "kind": "Declaration" + } + ], + "id": "\"f\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "f", "postConditions": [], @@ -16,15 +29,24 @@ "args": [ { "args": [ - "0", - "x" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "x" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "x", + { + "type": "int", + "var": "x" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -36,8 +58,12 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [] } @@ -45,7 +71,11 @@ "constructor": { "contract": "A", "initial storage": [], - "interface": "A()", + "interface": { + "args": [], + "id": "\"A\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -54,7 +84,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json index 019e7070..e44696c2 100644 --- a/tests/frontend/pass/token/transfer.act.typed.json +++ b/tests/frontend/pass/token/transfer.act.typed.json @@ -1,20 +1,38 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" } ], "contract": "Token", - "interface": "transfer(uint256 value, address to)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transfer", "postConditions": [], @@ -22,33 +40,40 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" }, { "args": [ - "value", { - "Pre": { + "type": "int", + "var": "value" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -59,7 +84,10 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" @@ -69,34 +97,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -113,15 +154,24 @@ "args": [ { "args": [ - "0", - "value" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "value", + { + "type": "int", + "var": "value" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -135,15 +185,24 @@ "args": [ { "args": [ - "0", - "to" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "to", + { + "type": "int", + "var": "to" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -157,26 +216,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -185,24 +248,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -217,26 +281,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -245,24 +316,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -277,7 +352,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -299,7 +377,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -319,53 +400,61 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "-" @@ -373,48 +462,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" @@ -428,14 +527,32 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "==" } ], "contract": "Token", - "interface": "transfer(uint256 value, address to)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transfer", "postConditions": [], @@ -443,33 +560,40 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" }, { "args": [ - "value", { - "Pre": { + "type": "int", + "var": "value" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -480,7 +604,10 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" @@ -490,34 +617,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -534,15 +674,24 @@ "args": [ { "args": [ - "0", - "value" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "value", + { + "type": "int", + "var": "value" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -556,15 +705,24 @@ "args": [ { "args": [ - "0", - "to" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "to", + { + "type": "int", + "var": "to" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -578,26 +736,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -606,24 +768,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -638,26 +801,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -666,24 +836,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -698,7 +872,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -720,7 +897,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -740,51 +920,58 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } } @@ -796,8 +983,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -805,7 +998,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "==" @@ -816,33 +1012,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -852,8 +1072,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -863,34 +1089,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -908,41 +1147,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -958,7 +1211,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -967,15 +1223,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -989,15 +1254,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1011,15 +1285,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -1033,26 +1316,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1061,24 +1348,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1093,30 +1381,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1125,28 +1421,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1161,26 +1462,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1189,24 +1497,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1221,26 +1533,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1249,24 +1568,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1281,7 +1604,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -1303,7 +1629,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -1323,101 +1652,119 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -1425,48 +1772,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -1483,8 +1840,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -1492,7 +1855,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" @@ -1504,40 +1870,54 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, { "args": [ { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" }, - "1" + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "-" @@ -1552,33 +1932,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1588,8 +1992,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -1599,34 +2009,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -1644,41 +2067,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -1694,7 +2131,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -1703,15 +2143,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1725,15 +2174,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1747,15 +2205,24 @@ "args": [ { "args": [ - "0", - "amount" - ], - "arity": 2, - "symbol": "<=" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } + ], + "arity": 2, + "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -1769,26 +2236,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1797,24 +2268,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1829,30 +2301,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1861,28 +2341,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1897,26 +2382,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1925,24 +2417,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1957,26 +2453,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1985,24 +2488,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2017,7 +2524,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -2039,7 +2549,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -2059,101 +2572,119 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2161,48 +2692,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -2219,8 +2760,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -2228,7 +2775,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" @@ -2240,40 +2790,54 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, { "args": [ { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" }, - "1" + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "-" @@ -2288,33 +2852,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2324,8 +2912,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -2335,34 +2929,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -2380,41 +2987,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2430,7 +3051,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -2439,15 +3063,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -2461,15 +3094,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -2483,15 +3125,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -2505,26 +3156,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2533,24 +3188,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2565,30 +3221,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2597,28 +3261,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2633,26 +3302,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2661,24 +3337,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2693,26 +3373,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2721,24 +3408,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2753,7 +3444,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -2775,7 +3469,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -2795,83 +3492,99 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2879,48 +3592,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2928,48 +3651,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -2982,41 +3715,71 @@ "case": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "==" } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3026,8 +3789,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -3037,34 +3806,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -3082,41 +3864,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -3132,7 +3928,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -3141,15 +3940,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -3163,15 +3971,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -3185,15 +4002,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3207,26 +4033,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3235,24 +4065,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3267,30 +4098,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3299,28 +4138,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3335,26 +4179,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3363,24 +4214,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3395,26 +4250,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3423,24 +4285,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3455,7 +4321,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -3477,7 +4346,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -3497,99 +4369,113 @@ } ], "returns": { - "expression": "1", - "sort": "int" + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", + "type": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "type": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } } @@ -3602,53 +4488,96 @@ { "location": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" + "type": "bytestring" }, - "value": "_name" + "value": { + "type": "bytestring", + "var": "_name" + } }, { "location": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" + "type": "bytestring" }, - "value": "_symbol" + "value": { + "type": "bytestring", + "var": "_symbol" + } }, { "location": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" + "type": "int" }, - "value": "_totalSupply" + "value": { + "type": "int", + "var": "_totalSupply" + } }, { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "type": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, - "value": "_totalSupply" + "value": { + "type": "int", + "var": "_totalSupply" + } } ], - "interface": "Token(string _symbol, string _name, string _version, uint256 _totalSupply)", + "interface": { + "args": [ + { + "abitype": "string", + "id": "\"_symbol\"", + "kind": "Declaration" + }, + { + "abitype": "string", + "id": "\"_name\"", + "kind": "Declaration" + }, + { + "abitype": "string", + "id": "\"_version\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"_totalSupply\"", + "kind": "Declaration" + } + ], + "id": "\"Token\"", + "kind": "Interface" + }, "invariants": [ { "contract": "Token", @@ -3658,15 +4587,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3681,14 +4619,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "_totalSupply" + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "==" @@ -3696,14 +4640,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Post" }, - "_totalSupply" + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "==" @@ -3714,14 +4664,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3730,12 +4686,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3756,15 +4715,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3779,14 +4747,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Pre" }, - "_name" + { + "type": "bytestring", + "var": "_name" + } ], "arity": 2, "symbol": "==" @@ -3794,14 +4768,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Post" }, - "_name" + { + "type": "bytestring", + "var": "_name" + } ], "arity": 2, "symbol": "==" @@ -3817,15 +4797,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3840,14 +4829,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Pre" }, - "_symbol" + { + "type": "bytestring", + "var": "_symbol" + } ], "arity": 2, "symbol": "==" @@ -3855,14 +4850,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Post" }, - "_symbol" + { + "type": "bytestring", + "var": "_symbol" + } ], "arity": 2, "symbol": "==" @@ -3878,15 +4879,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3900,7 +4910,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -3923,42 +4936,93 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { "Token": { "allowance": [ { - "ixTypes": "[address,address]", - "type": "mapping", - "valType": "uint256" + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + }, + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 4 ], "balanceOf": [ { - "ixTypes": "[address]", - "type": "mapping", - "valType": "uint256" + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 3 ], "name": [ { - "type": "string" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } }, 0 ], "symbol": [ { - "type": "string" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } }, 1 ], "totalSupply": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 2 ]