CLI and JSON tests

test/cmdlineTests/model_checker_invariants_all/args

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

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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
+((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+<errorCode> = 3 -> Assertion failed at assert(x < 10)

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

test/cmdlineTests/model_checker_invariants_contract/args

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

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)

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

test/cmdlineTests/model_checker_invariants_contract_reentrancy/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-invariants contract,reentrancy

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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
+((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+<errorCode> = 3 -> Assertion failed at assert(x < 10)

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

test/cmdlineTests/model_checker_invariants_reentrancy/args

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

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) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)

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

test/cmdlineTests/model_checker_invariants_wrong/args

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

test/cmdlineTests/model_checker_invariants_wrong/err

@@ -0,0 +1 @@
+Invalid option for --model-checker-invariants: what

test/cmdlineTests/model_checker_invariants_wrong/exit

@@ -0,0 +1 @@
+1

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

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

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

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

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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
+((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+<errorCode> = 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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
+((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+<errorCode> = 3 -> Assertion failed at assert(x < 10)
+","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

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

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) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+
+
+","message":"Reentrancy property(ies) for A:test:
+((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+<errorCode> = 0 -> no errors
+<errorCode> = 1 -> Assertion failed at assert(x < 10)
+","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

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

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

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

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

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

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