From 6c58f31b4ac0484715ed1105ac4a78b38d7473f3 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 15 Mar 2023 17:52:58 +0100 Subject: [PATCH] add cli tests --- .../args | 1 + .../err | 1 + .../input.sol | 7 ++++ .../args | 1 + .../err | 1 + .../input.sol | 7 ++++ .../args | 1 + .../err | 1 + .../input.sol | 7 ++++ .../args | 1 + .../err | 5 +++ .../input.sol | 7 ++++ .../args | 1 + .../err | 5 +++ .../input.sol | 7 ++++ .../args | 1 + .../err | 5 +++ .../input.sol | 7 ++++ .../input.json | 21 ++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 21 ++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 21 ++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 27 ++++++++++++++++ .../output.json | 32 +++++++++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 22 +++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 32 +++++++++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 32 +++++++++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 32 +++++++++++++++++++ .../input.json | 22 +++++++++++++ .../output.json | 12 +++++++ 40 files changed, 582 insertions(+) create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_all_engines/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_all_engines/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_all_engines/input.sol create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_bmc/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_bmc/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_bmc/input.sol create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_chc/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_chc/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_default_chc/input.sol create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_all_engines/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_all_engines/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_all_engines/input.sol create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_bmc/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_bmc/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_bmc/input.sol create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_chc/args create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_chc/err create mode 100644 test/cmdlineTests/model_checker_show_unsupported_true_chc/input.sol create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_wrong/input.json create mode 100644 test/cmdlineTests/standard_model_checker_show_unsupported_wrong/output.json diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/args b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/args new file mode 100644 index 000000000..5aeb1490e --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/err b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/err new file mode 100644 index 000000000..578846b36 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/err @@ -0,0 +1 @@ +Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them. diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_all_engines/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_bmc/args b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/args new file mode 100644 index 000000000..549f20236 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_bmc/err b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/err new file mode 100644 index 000000000..578846b36 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/err @@ -0,0 +1 @@ +Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them. diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_bmc/input.sol b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_bmc/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_chc/args b/test/cmdlineTests/model_checker_show_unsupported_default_chc/args new file mode 100644 index 000000000..7458a47d3 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_chc/err b/test/cmdlineTests/model_checker_show_unsupported_default_chc/err new file mode 100644 index 000000000..578846b36 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_chc/err @@ -0,0 +1 @@ +Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them. diff --git a/test/cmdlineTests/model_checker_show_unsupported_default_chc/input.sol b/test/cmdlineTests/model_checker_show_unsupported_default_chc/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_default_chc/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/args b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/args new file mode 100644 index 000000000..c0e876742 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-show-unsupported diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/err b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/err new file mode 100644 index 000000000..53c664ffc --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/err @@ -0,0 +1,5 @@ +Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> model_checker_show_unsupported_true_all_engines/input.sol:5:9: + | +5 | assembly {} + | ^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/input.sol b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_all_engines/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_bmc/args b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/args new file mode 100644 index 000000000..ab152ae20 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-show-unsupported diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_bmc/err b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/err new file mode 100644 index 000000000..013a7b0f1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/err @@ -0,0 +1,5 @@ +Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> model_checker_show_unsupported_true_bmc/input.sol:5:9: + | +5 | assembly {} + | ^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_bmc/input.sol b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_bmc/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_chc/args b/test/cmdlineTests/model_checker_show_unsupported_true_chc/args new file mode 100644 index 000000000..16821838d --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-show-unsupported diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_chc/err b/test/cmdlineTests/model_checker_show_unsupported_true_chc/err new file mode 100644 index 000000000..8dad0cc65 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_chc/err @@ -0,0 +1,5 @@ +Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> model_checker_show_unsupported_true_chc/input.sol:5:9: + | +5 | assembly {} + | ^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_show_unsupported_true_chc/input.sol b/test/cmdlineTests/model_checker_show_unsupported_true_chc/input.sol new file mode 100644 index 000000000..72a8049c1 --- /dev/null +++ b/test/cmdlineTests/model_checker_show_unsupported_true_chc/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f() external pure { + assembly {} + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/input.json new file mode 100644 index 000000000..c307217c6 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/input.json @@ -0,0 +1,21 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_all_engines/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/input.json new file mode 100644 index 000000000..668a60e00 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/input.json @@ -0,0 +1,21 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_bmc/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/input.json new file mode 100644 index 000000000..360235eb4 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/input.json @@ -0,0 +1,21 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_default_chc/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/input.json new file mode 100644 index 000000000..10092aa6f --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnsupported": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/input.json new file mode 100644 index 000000000..e3a42c295 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/input.json @@ -0,0 +1,27 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + struct S { + uint x; + } + S s; + function f(bool b) public { + s.x |= b ? 1 : 2; + assert(s.x > 0); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnsupported": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/output.json new file mode 100644 index 000000000..fb599d21d --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_all_engines/standard_model_checker_show_unsupported_false_all_enginesstandard_model_checker_show_unsupported_false_bmc/output.json @@ -0,0 +1,32 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5840", + "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + +", + "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", + "severity": "warning", + "type": "Warning" + }, + { + "component": "general", + "errorCode": "2788", + "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + +", + "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/input.json new file mode 100644 index 000000000..7d15e6d7f --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "showUnsupported": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_bmc/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/input.json new file mode 100644 index 000000000..4d5a79c6d --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "showUnsupported": false + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/output.json new file mode 100644 index 000000000..23cf80def --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_false_chc/output.json @@ -0,0 +1,22 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "5724", + "formattedMessage": "Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them. + +", + "message": "SMTChecker: 1 unsupported language feature(s). Enable the model checker option \"show unsupported\" to see all of them.", + "severity": "warning", + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/input.json new file mode 100644 index 000000000..c1fbeab1b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnsupported": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/output.json new file mode 100644 index 000000000..13d327d40 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_all_engines/output.json @@ -0,0 +1,32 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "7737", + "formattedMessage": "Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> A:6:7: + | +6 | \t\t\t\t\t\tassembly {} + | \t\t\t\t\t\t^^^^^^^^^^^ + +", + "message": "Inline assembly may cause SMTChecker to produce spurious warnings (false positives).", + "severity": "warning", + "sourceLocation": + { + "end": 127, + "file": "A", + "start": 116 + }, + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/input.json new file mode 100644 index 000000000..38e5cb7a7 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "showUnsupported": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/output.json new file mode 100644 index 000000000..13d327d40 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_bmc/output.json @@ -0,0 +1,32 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "7737", + "formattedMessage": "Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> A:6:7: + | +6 | \t\t\t\t\t\tassembly {} + | \t\t\t\t\t\t^^^^^^^^^^^ + +", + "message": "Inline assembly may cause SMTChecker to produce spurious warnings (false positives).", + "severity": "warning", + "sourceLocation": + { + "end": 127, + "file": "A", + "start": 116 + }, + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/input.json new file mode 100644 index 000000000..f84ca4610 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "showUnsupported": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/output.json new file mode 100644 index 000000000..13d327d40 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_true_chc/output.json @@ -0,0 +1,32 @@ +{ + "errors": + [ + { + "component": "general", + "errorCode": "7737", + "formattedMessage": "Warning: Inline assembly may cause SMTChecker to produce spurious warnings (false positives). + --> A:6:7: + | +6 | \t\t\t\t\t\tassembly {} + | \t\t\t\t\t\t^^^^^^^^^^^ + +", + "message": "Inline assembly may cause SMTChecker to produce spurious warnings (false positives).", + "severity": "warning", + "sourceLocation": + { + "end": 127, + "file": "A", + "start": 116 + }, + "type": "Warning" + } + ], + "sources": + { + "A": + { + "id": 0 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/input.json b/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/input.json new file mode 100644 index 000000000..9fa8f5a59 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test { + function f() external pure { + assembly {} + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "showUnsupported": "aaa" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/output.json b/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/output.json new file mode 100644 index 000000000..997b005ef --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_show_unsupported_wrong/output.json @@ -0,0 +1,12 @@ +{ + "errors": + [ + { + "component": "general", + "formattedMessage": "settings.modelChecker.showUnsupported must be a Boolean value.", + "message": "settings.modelChecker.showUnsupported must be a Boolean value.", + "severity": "error", + "type": "JSONError" + } + ] +}