Error during testContract.sol analyzing

[beksaev]

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