search

eth-sri / securify2

Securify v2.0
Apache License 2.0
589 stars 135 forks source link

Error during testContract.sol analyzing #35

Open beksaev opened 2 years ago

beksaev commented 2 years ago

Environment:

solcVersion: 0.8.11+commit.d7f03943.Darwin.appleclang souffle version 2.2

When securify ./securify/staticanalysis/testContract.sol

get such errors:

pragma directive defines a prior version to 0.8.11. Changing pragma version to 0.8.11.... Traceback (most recent call last): File "/Users/nikolaybeksaev/Projects/securify2/securify2/venv/bin/securify", line 33, in sys.exit(load_entry_point('securify', 'console_scripts', 'securify')()) File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/main.py", line 268, in main patterns = get_list_of_patterns(context=context, File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/main.py", line 15, in get_list_of_patterns pattern_classes = discover_patterns() File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/analyses/analysis.py", line 123, in discover_patterns patterns.update(c.get()) File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/analyses/patterns/static/static_analysis_patterns.py", line 16, in get patterns = cls.list_static_patterns() File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/analyses/patterns/static/static_analysis_patterns.py", line 23, in list_static_patterns patterns = static_analysis.discover_patterns() File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/staticanalysis/static_analysis.py", line 63, in discover_patterns souffle_output, facts_out = souffle.run_souffle( File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/staticanalysis/souffle/souffle.py", line 57, in run_souffle souffle_output = souffle_wrapper( File "/Users/nikolaybeksaev/Projects/securify2/securify2/securify/staticanalysis/souffle/wrapper.py", line 114, in souffle_wrapper raise SouffleError( securify.staticanalysis.souffle.exceptions.SouffleError: Error during souffle execution:
Warning: Deprecated type declaration used in file analysis-input.dl at line 3 .number_type ArgIndex // Index used to qualify block arguments ^----------------------------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 4 .symbol_type StateVar // Identifier for state variables ^---------------------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 5 .symbol_type Transfer // ID of a transfer between blocks ^----------------------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 6 .symbol_type Name // Name associated to an object ^-------------------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 7 .symbol_type SSA // ID of a statement or block argument and its value ^----------------------------------------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 8 .symbol_type Block // ID of a basic block ^----------------------------------------------- Warning: Deprecated type declaration used in file analysis-input.dl at line 9 .symbol_type Contract // ID of a contract ^-------------------------------------------- Warning: Deprecated type declaration used in file analysis-patterns.dl at line 1 .symbol_type PatternId ^---------------------- Warning: Deprecated type declaration used in file analysis-patterns.dl at line 4 .number_type MatchId ^-------------------- Warning: Deprecated type declaration used in file analysis-patterns.dl at line 5 .symbol_type MatchType ^---------------------- Warning: Deprecated type declaration used in file analysis-patterns.dl at line 6 .symbol_type MatchComment ^------------------------- Warning: No rules/facts defined for relation patternUnusedStateVariablePattern.compliance in file analysis-patterns.dl at line 29 .decl compliance(element: Element, info: symbol, comment: symbol) -------^----------------------------------------------------------- Warning: Deprecated type declaration used in file callstack-context.dl at line 3 .symbol_type CallStackTag ^------------------------- Warning: Variable callerFunction only occurs once in file callstack-context.dl at line 20 callerContext = [callerFunction, callerTransfers, "precise"], -------------------------^-------------------------------------------- Warning: Variable callDepth only occurs once in file callstack-context.dl at line 27 transferStacks.length(callerTransfers, callDepth), -----------------------------------------------^----------- Warning: Variable callerFunction only occurs once in file callstack-context.dl at line 28 callerContext = [callerFunction, callerTransfers, callerTag], -------------------------^-------------------------------------------- Warning: Variable callerFunction only occurs once in file callstack-context.dl at line 37 callerContext = [callerFunction, callerTransfers, callerTag], -------------------------^-------------------------------------------- Warning: Variable callerTransfers only occurs once in file callstack-context.dl at line 37 callerContext = [callerFunction, callerTransfers, callerTag], -----------------------------------------^---------------------------- Warning: Variable callerTag only occurs once in file callstack-context.dl at line 37 callerContext = [callerFunction, callerTransfers, callerTag], ----------------------------------------------------------^----------- Warning: No rules/facts defined for relation patternIncorrectInequalityPattern.compliantInContext in file abstract-context-pattern.dl at line 9 .decl compliantInContext(element: ctxProvider.ElementInContext, comment: MatchComment) -------^-------------------------------------------------------------------------------- Warning: Variable comment only occurs once in file abstract-context-pattern.dl at line 26 violationInContext([element, ctx], comment), ctxProvider.contextToString(ctx, ctxString). -------------------------------------^------------------------------------------------------ Warning: Variable ctxString only occurs once in file abstract-context-pattern.dl at line 26 violationInContext([element, ctx], comment), ctxProvider.contextToString(ctx, ctxString). --------------------------------------------------------------------------------^----------- Error: Atom's argument type is not a subtype of its declared type in file locked-ether.dl at line 15 contractCompliance(contract, matchComment) :- -----------------------^-------------------------- The argument's declared type is Contract in file abstract-contract-pattern.dl at line 26 .decl contractCompliance(contract: Contract, comment: MatchComment) ------------------------------------^-------------------------------- Warning: Variable argInContext only occurs once in file pass.dl at line 27 ctxProvider.elementInContext(argInContext, argument, context), -------------------------------------^--------------------------------- Error: Atom's argument type is not a subtype of its declared type in file timestamp.dl at line 53 existsBlockTimestamp(timestampSSA, blockTimestampLine):- ---------------------------------------^--------------------- The argument's declared type is Element in file timestamp.dl at line 52 .decl existsBlockTimestamp(blockTimestamp: Element, blockTimestampLine: Element) ----------------------------------------------------------------------------^-------- Error: Atom's argument type is not a subtype of its declared type in file tx-origin.dl at line 37 callInfo(call, matchInfo, matchComment) :- -------------^--------------------------------- The argument's declared type is Transfer in file tx-origin.dl at line 36 .decl callInfo(call: Transfer, matchInfo: symbol, matchComment: symbol) -------------------------^-------------------------------------------------- Warning: Variable valueCtx only occurs once in file unrestricted-ether-flow.dl at line 38 ctxProvider.elementInContext(valueCtx, value, context), -------------------------------------^-------------------------- Warning: Variable thisBlock only occurs once in file unused-return.dl at line 11 externalJump(thisBlock, otherBlock, returnBlock), ---------------------^------------------------------------ Warning: Deprecated type declaration used in file util-sets.dl at line 5 .symbol_type Set -^---------------- Warning: Variable _c marked as singleton but occurs more than once in file semantics.dl at line 23 criticalUsageAt(val, call) :- externalCall(c), callValue(c, v), SAME_CTX(val, call, v, c).

Warning: Variable _c marked as singleton but occurs more than once in file semantics.dl at line 24 criticalUsageAt(gas, call) :- externalCall(c), callGas(c, g), SAME_CTX(gas, call, g, c).

Warning: Variable _c marked as singleton but occurs more than once in file semantics.dl at line 27 SAME_CTX(arg, call, a, c).

Warning: Variable _c marked as singleton but occurs more than once in file semantics.dl at line 31 SAME_CTX(arg, ret, a, r).

Warning: Variable _c marked as singleton but occurs more than once in file semantics.dl at line 33 criticalUsageAt(value, store) :- storageMutation(s, v), SAME_CTX(value, store, v, s).

Error: Atom's argument type is not a subtype of its declared type in file trusted-variable.dl at line 29 trustedPredecessors(node, SET_ADD(set, [pred])) :- -------------------------------^----------------------- The argument's declared type is Set in file trusted-variable.dl at line 12 .decl trustedPredecessors(node: data.Node, preds: Set) ------------------------------------------------------^---- Error: Ambiguous record in file trusted-variable.dl at line 29 trustedPredecessors(node, SET_ADD(set, [pred])) :- ---------------------------------------------^--------- Warning: No rules/facts defined for relation warnings in file util-debug.dl at line 5 .decl warnings(error: symbol) ------^----------------------- 5 errors generated, evaluation aborted