add cli tests

test/cmdlineTests/model_checker_show_unsupported_default_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all

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.

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 {}
+    }
+}

test/cmdlineTests/model_checker_show_unsupported_default_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc

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.

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 {}
+    }
+}

test/cmdlineTests/model_checker_show_unsupported_default_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc

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.

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 {}
+    }
+}

test/cmdlineTests/model_checker_show_unsupported_true_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-show-unsupported

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 {}
+  |         ^^^^^^^^^^^

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 {}
+    }
+}

test/cmdlineTests/model_checker_show_unsupported_true_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-show-unsupported

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 {}
+  |         ^^^^^^^^^^^

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 {}
+    }
+}

test/cmdlineTests/model_checker_show_unsupported_true_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-show-unsupported

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 {}
+  |         ^^^^^^^^^^^

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 {}
+    }
+}

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"
+		}
+	}
+}

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
+        }
+    }
+}

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"
+		}
+	}
+}

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
+        }
+    }
+}

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"
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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
+		}
+	}
+}

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
+        }
+    }
+}

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"
+		}
+	}
+}

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"
+        }
+    ]
+}