diff --git a/test/cmdlineTests/model_checker_invariants_all/args b/test/cmdlineTests/model_checker_invariants_all/args new file mode 100644 index 000000000..389acc647 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants all diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err new file mode 100644 index 000000000..47bc04256 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/err @@ -0,0 +1,15 @@ +Warning: Return value of low-level calls not used. + --> model_checker_invariants_all/input.sol:6:3: + | +6 | _a.call(""); + | ^^^^^^^^^^^ + +Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test: +(x <= 0) +Reentrancy property(ies) for model_checker_invariants_all/input.sol:test: +(!(x <= 0) || (x' <= 0)) +((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_all/input.sol b/test/cmdlineTests/model_checker_invariants_all/input.sol new file mode 100644 index 000000000..f8601cf4f --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + uint x; + function f(address _a) public { + _a.call(""); + assert(x < 10); + } + function g() public view { + assert(x < 10); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_contract/args b/test/cmdlineTests/model_checker_invariants_contract/args new file mode 100644 index 000000000..e856a73b9 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants contract diff --git a/test/cmdlineTests/model_checker_invariants_contract/err b/test/cmdlineTests/model_checker_invariants_contract/err new file mode 100644 index 000000000..a5277bebf --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/err @@ -0,0 +1,2 @@ +Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test: +(x <= 0) diff --git a/test/cmdlineTests/model_checker_invariants_contract/input.sol b/test/cmdlineTests/model_checker_invariants_contract/input.sol new file mode 100644 index 000000000..3a857d484 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + uint x; + function f() public view { + assert(x < 10); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args new file mode 100644 index 000000000..90591a5ae --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants contract,reentrancy diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err new file mode 100644 index 000000000..372143657 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err @@ -0,0 +1,15 @@ +Warning: Return value of low-level calls not used. + --> model_checker_invariants_contract_reentrancy/input.sol:6:3: + | +6 | _a.call(""); + | ^^^^^^^^^^^ + +Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test: +(x <= 0) +Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test: +(!(x <= 0) || (x' <= 0)) +((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol new file mode 100644 index 000000000..f8601cf4f --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + uint x; + function f(address _a) public { + _a.call(""); + assert(x < 10); + } + function g() public view { + assert(x < 10); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/args b/test/cmdlineTests/model_checker_invariants_reentrancy/args new file mode 100644 index 000000000..904defe84 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants reentrancy diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/err b/test/cmdlineTests/model_checker_invariants_reentrancy/err new file mode 100644 index 000000000..a2fd6075a --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/err @@ -0,0 +1,10 @@ +Warning: Return value of low-level calls not used. + --> model_checker_invariants_reentrancy/input.sol:6:3: + | +6 | _a.call(""); + | ^^^^^^^^^^^ + +Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test: +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol new file mode 100644 index 000000000..f21d4d4c8 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + uint x; + function f(address _a) public { + _a.call(""); + assert(x < 10); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_wrong/args b/test/cmdlineTests/model_checker_invariants_wrong/args new file mode 100644 index 000000000..ae601a044 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants what diff --git a/test/cmdlineTests/model_checker_invariants_wrong/err b/test/cmdlineTests/model_checker_invariants_wrong/err new file mode 100644 index 000000000..1dc94780d --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/err @@ -0,0 +1 @@ +Invalid option for --model-checker-invariants: what diff --git a/test/cmdlineTests/model_checker_invariants_wrong/exit b/test/cmdlineTests/model_checker_invariants_wrong/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_invariants_wrong/input.sol b/test/cmdlineTests/model_checker_invariants_wrong/input.sol new file mode 100644 index 000000000..17bf3b749 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + uint x; + function g() public view { + assert(x < 10); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract/input.json new file mode 100644 index 000000000..d47c93de2 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f() public view { + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": ["contract"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json new file mode 100644 index 000000000..1cd236baf --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json @@ -0,0 +1,7 @@ +{"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test: +(x <= 0) + + +","message":"Contract invariant(s) for A:test: +(x <= 0) +","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json new file mode 100644 index 000000000..56139e6a5 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f(address _a) public { + _a.call(\"\"); + assert(x < 10); + } + function g() public view { + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": ["contract", "reentrancy"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json new file mode 100644 index 000000000..433648d0b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json @@ -0,0 +1,27 @@ +{"errors":[{"component":"general","errorCode":"9302","formattedMessage":"Warning: Return value of low-level calls not used. + --> A:7:7: + | +7 | \t\t\t\t\t\t_a.call(\"\"); + | \t\t\t\t\t\t^^^^^^^^^^^ + +","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test: +(x <= 0) +Reentrancy property(ies) for A:test: +(!(x <= 0) || (x' <= 0)) +((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) + + +","message":"Contract invariant(s) for A:test: +(x <= 0) +Reentrancy property(ies) for A:test: +(!(x <= 0) || (x' <= 0)) +((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) +","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json new file mode 100644 index 000000000..1f98000b0 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json @@ -0,0 +1,24 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f(address _a) public { + _a.call(\"\"); + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": ["reentrancy"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json new file mode 100644 index 000000000..4158c3ae1 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json @@ -0,0 +1,17 @@ +{"errors":[{"component":"general","errorCode":"9302","formattedMessage":"Warning: Return value of low-level calls not used. + --> A:7:7: + | +7 | \t\t\t\t\t\t_a.call(\"\"); + | \t\t\t\t\t\t^^^^^^^^^^^ + +","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Reentrancy property(ies) for A:test: +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + + +","message":"Reentrancy property(ies) for A:test: +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) +","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json new file mode 100644 index 000000000..e8ee6aba6 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f() public view { + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": ["what"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json new file mode 100644 index 000000000..7758b29ca --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"Invalid model checker invariants requested.","message":"Invalid model checker invariants requested.","severity":"error","type":"JSONError"}]} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json new file mode 100644 index 000000000..54fc96d46 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f() public view { + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": [2] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json new file mode 100644 index 000000000..5ad18a3b1 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"Every invariant type in settings.modelChecker.invariants must be a string.","message":"Every invariant type in settings.modelChecker.invariants must be a string.","severity":"error","type":"JSONError"}]} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json new file mode 100644 index 000000000..f7522e6e5 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + uint x; + function f() public view { + assert(x < 10); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "invariants": 2 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json new file mode 100644 index 000000000..b4fba3576 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.invariants must be an array.","message":"settings.modelChecker.invariants must be an array.","severity":"error","type":"JSONError"}]}