Skip to content

Commit 03cec31

Browse files
yoav-el-certorayoav-el-certora
authored
8.2.0 Release
fcfd4371c0e5dc054903076b0c3129eceb43dce7
2 parents b6b9f58 + 76c6ce0 commit 03cec31

File tree

450 files changed

+17618
-2528
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

450 files changed

+17618
-2528
lines changed

‎Public/CITests/testCertoraClient.py‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -851,8 +851,15 @@ def check_run(expect: List[str]) -> None:
851851
remapping = "a=lib\na=lib"
852852
with open(Util.REMAPPINGS_FILE, "w") as file:
853853
file.write(remapping)
854-
description = f"duplicates in {Util.REMAPPINGS_FILE}"
855-
suite.expect_failure(description=description, expected="remappings.txt includes duplicated")
854+
description = f"identical duplicates in {Util.REMAPPINGS_FILE}"
855+
suite.expect_success(description=description)
856+
Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
857+
858+
remapping = "a=lib\na=lib2"
859+
with open(Util.REMAPPINGS_FILE, "w") as file:
860+
file.write(remapping)
861+
description = f"non-identical duplicates in {Util.REMAPPINGS_FILE}"
862+
suite.expect_failure(description=description, expected="Conflicting values in remappings.txt for key 'a'")
856863
Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
857864

858865
remapping = '{"dependencies": {"c": "^3.4.1"},"devDependencies": {"c": "^5.0.8"}}'
@@ -871,6 +878,15 @@ def check_run(expect: List[str]) -> None:
871878
description = f"duplicates in {Util.REMAPPINGS_FILE} and Util.PACKAGE_FILE"
872879
suite.expect_failure(description=description, expected="package.json and remappings.txt include duplicated")
873880
Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
881+
Path(Util.PACKAGE_FILE).unlink(missing_ok=True)
882+
883+
884+
remapping = "a=lib\nb=lib=lib2"
885+
with open(Util.REMAPPINGS_FILE, "w") as file:
886+
file.write(remapping)
887+
888+
description = f"remappings.txt with bad format"
889+
suite.expect_failure(description=description, expected="Invalid remapping in remappings.txt")
874890
Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
875891

876892
def test_solc_args(self) -> None:

‎Public/CITests/testMutateClient.py‎

Lines changed: 38 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -92,10 +92,43 @@ def test_conf_file_inputs(self) -> None:
9292
expected='skip_validate not allowed inside embedded gambit object')
9393
suite = MutantTestSuite(conf_file_template=_p('mutation_template.conf'),
9494
test_attribute=Util.TestValue.CHECK_ARGS)
95-
suite.expect_failure(description="outdir without gambit",
95+
suite.expect_failure(description="outdir without gambit being set",
9696
replacements=TestUtil.replace_x(f'{mutation_expr()}, "outdir": "new_dir"'),
9797
expected="Invalid configuration: 'outdir' should not be set")
9898

99+
not_a_list = f'"manual_mutants": {{ "file_to_mutate": "{_p("A.sol")}", "mutants_location": "{_p("A_mutations")}"}}'
100+
suite.expect_failure(description="manual_mutants is not a list",
101+
replacements=TestUtil.replace_x(not_a_list),
102+
expected="manual_mutants should be a list of objects")
103+
104+
not_an_object = f'"manual_mutants": ["not an object", "also not an object"]'
105+
suite.expect_failure(description="manual_mutants is not a list of objects",
106+
replacements=TestUtil.replace_x(not_an_object),
107+
expected="manual_mutants should be a list of objects")
108+
109+
110+
missing_key = f'"manual_mutants": [{{ "mutants_location": "{_p("A_mutations")}"}}]'
111+
suite.expect_failure(description="missing mandatory file_to_mutate",
112+
replacements=TestUtil.replace_x(missing_key),
113+
expected="manual_mutants object must contain keys:")
114+
115+
116+
unknown_key = f'"manual_mutants": [{{ "file_to_mutate": "{_p("A.sol")}", "mutants_location": "{_p("A_mutations")}", "unknown": "{_p("A_mutations")}"}}]'
117+
suite.expect_failure(description="manual_mutants object contains unknown key",
118+
replacements=TestUtil.replace_x(unknown_key),
119+
expected="manual_mutants object contains invalid keys")
120+
121+
122+
bad_file = f'"manual_mutants": [{{ "file_to_mutate": "{_p("bad.sol")}", "mutants_location": "{_p("A_mutations")}"}}]'
123+
suite.expect_failure(description="manual_mutants object missing file_to_mutate",
124+
replacements=TestUtil.replace_x(bad_file),
125+
expected="Invalid file_to_mutate in manual mutant")
126+
127+
bad_location = f'"manual_mutants": [{{ "file_to_mutate": "{_p("A.sol")}", "mutants_location": "{_p("bad_location")}"}}]'
128+
suite.expect_failure(description="manual_mutants object missing file_to_mutate",
129+
replacements=TestUtil.replace_x(bad_location),
130+
expected="Invalid mutants location")
131+
99132
def test_invalid_runs(self) -> None:
100133
suite = MutantTestSuite(conf_file_template=_p('mutation_conf_top_level.conf'),
101134
test_attribute=Util.TestValue.CHECK_ARGS)
@@ -154,7 +187,7 @@ def test_compile_mutation(self) -> None:
154187
mutation_attrs['manual_mutants'][0]['mutants_location'] = "does_not_exist"
155188
suite.expect_failure(description="single manual mutation - bad location",
156189
replacements=TestUtil.replace_x(TestUtil.json_to_str(mutation_attrs)),
157-
expected="not a valid file or directory")
190+
expected="Invalid mutants location")
158191

159192
def test_mutations_flags(self) -> None:
160193

@@ -281,4 +314,6 @@ def test_collect_bad_origin(self) -> None:
281314

282315
if __name__ == '__main__':
283316
test_argv = [f"{sys.argv[1]}, {sys.argv[2]}"]
284-
unittest.main(argv=test_argv, exit=False)
317+
runner = unittest.main(argv=test_argv, exit=False)
318+
if not runner.result.wasSuccessful():
319+
exit(1)

‎Public/TestEVM/CVLCompilation/BWNot/C.sol‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
contract C {
2+
function solBWNot1(bytes1 b) external pure returns (bytes1) {
3+
return ~b;
4+
}
5+
function solBWNot2(bytes2 b) external pure returns (bytes2) {
6+
return ~b;
7+
}
8+
function solBWNot3(bytes3 b) external pure returns (bytes3) {
9+
return ~b;
10+
}
11+
function solBWNot4(bytes4 b) external pure returns (bytes4) {
12+
return ~b;
13+
}
14+
function solBWNot5(bytes5 b) external pure returns (bytes5) {
15+
return ~b;
16+
}
17+
function solBWNot6(bytes6 b) external pure returns (bytes6) {
18+
return ~b;
19+
}
20+
function solBWNot7(bytes7 b) external pure returns (bytes7) {
21+
return ~b;
22+
}
23+
function solBWNot8(bytes8 b) external pure returns (bytes8) {
24+
return ~b;
25+
}
26+
function solBWNot9(bytes9 b) external pure returns (bytes9) {
27+
return ~b;
28+
}
29+
function solBWNot10(bytes10 b) external pure returns (bytes10) {
30+
return ~b;
31+
}
32+
function solBWNot11(bytes11 b) external pure returns (bytes11) {
33+
return ~b;
34+
}
35+
function solBWNot12(bytes12 b) external pure returns (bytes12) {
36+
return ~b;
37+
}
38+
function solBWNot13(bytes13 b) external pure returns (bytes13) {
39+
return ~b;
40+
}
41+
function solBWNot14(bytes14 b) external pure returns (bytes14) {
42+
return ~b;
43+
}
44+
function solBWNot15(bytes15 b) external pure returns (bytes15) {
45+
return ~b;
46+
}
47+
function solBWNot16(bytes16 b) external pure returns (bytes16) {
48+
return ~b;
49+
}
50+
function solBWNot17(bytes17 b) external pure returns (bytes17) {
51+
return ~b;
52+
}
53+
function solBWNot18(bytes18 b) external pure returns (bytes18) {
54+
return ~b;
55+
}
56+
function solBWNot19(bytes19 b) external pure returns (bytes19) {
57+
return ~b;
58+
}
59+
function solBWNot20(bytes20 b) external pure returns (bytes20) {
60+
return ~b;
61+
}
62+
function solBWNot21(bytes21 b) external pure returns (bytes21) {
63+
return ~b;
64+
}
65+
function solBWNot22(bytes22 b) external pure returns (bytes22) {
66+
return ~b;
67+
}
68+
function solBWNot23(bytes23 b) external pure returns (bytes23) {
69+
return ~b;
70+
}
71+
function solBWNot24(bytes24 b) external pure returns (bytes24) {
72+
return ~b;
73+
}
74+
function solBWNot25(bytes25 b) external pure returns (bytes25) {
75+
return ~b;
76+
}
77+
function solBWNot26(bytes26 b) external pure returns (bytes26) {
78+
return ~b;
79+
}
80+
function solBWNot27(bytes27 b) external pure returns (bytes27) {
81+
return ~b;
82+
}
83+
function solBWNot28(bytes28 b) external pure returns (bytes28) {
84+
return ~b;
85+
}
86+
function solBWNot29(bytes29 b) external pure returns (bytes29) {
87+
return ~b;
88+
}
89+
function solBWNot30(bytes30 b) external pure returns (bytes30) {
90+
return ~b;
91+
}
92+
function solBWNot31(bytes31 b) external pure returns (bytes31) {
93+
return ~b;
94+
}
95+
function solBWNot32(bytes32 b) external pure returns (bytes32) {
96+
return ~b;
97+
}
98+
99+
/**
100+
for x in range(0,32):
101+
print(f"function solBWNot{x+1}UInt(uint{8*(x+1)} b) external pure returns (uint{8*(x+1)})" + " { return ~b; }")
102+
*/
103+
function solBWNot1UInt(uint8 b) external pure returns (uint8) { return ~b; }
104+
function solBWNot2UInt(uint16 b) external pure returns (uint16) { return ~b; }
105+
function solBWNot3UInt(uint24 b) external pure returns (uint24) { return ~b; }
106+
function solBWNot4UInt(uint32 b) external pure returns (uint32) { return ~b; }
107+
function solBWNot5UInt(uint40 b) external pure returns (uint40) { return ~b; }
108+
function solBWNot6UInt(uint48 b) external pure returns (uint48) { return ~b; }
109+
function solBWNot7UInt(uint56 b) external pure returns (uint56) { return ~b; }
110+
function solBWNot8UInt(uint64 b) external pure returns (uint64) { return ~b; }
111+
function solBWNot9UInt(uint72 b) external pure returns (uint72) { return ~b; }
112+
function solBWNot10UInt(uint80 b) external pure returns (uint80) { return ~b; }
113+
function solBWNot11UInt(uint88 b) external pure returns (uint88) { return ~b; }
114+
function solBWNot12UInt(uint96 b) external pure returns (uint96) { return ~b; }
115+
function solBWNot13UInt(uint104 b) external pure returns (uint104) { return ~b; }
116+
function solBWNot14UInt(uint112 b) external pure returns (uint112) { return ~b; }
117+
function solBWNot15UInt(uint120 b) external pure returns (uint120) { return ~b; }
118+
function solBWNot16UInt(uint128 b) external pure returns (uint128) { return ~b; }
119+
function solBWNot17UInt(uint136 b) external pure returns (uint136) { return ~b; }
120+
function solBWNot18UInt(uint144 b) external pure returns (uint144) { return ~b; }
121+
function solBWNot19UInt(uint152 b) external pure returns (uint152) { return ~b; }
122+
function solBWNot20UInt(uint160 b) external pure returns (uint160) { return ~b; }
123+
function solBWNot21UInt(uint168 b) external pure returns (uint168) { return ~b; }
124+
function solBWNot22UInt(uint176 b) external pure returns (uint176) { return ~b; }
125+
function solBWNot23UInt(uint184 b) external pure returns (uint184) { return ~b; }
126+
function solBWNot24UInt(uint192 b) external pure returns (uint192) { return ~b; }
127+
function solBWNot25UInt(uint200 b) external pure returns (uint200) { return ~b; }
128+
function solBWNot26UInt(uint208 b) external pure returns (uint208) { return ~b; }
129+
function solBWNot27UInt(uint216 b) external pure returns (uint216) { return ~b; }
130+
function solBWNot28UInt(uint224 b) external pure returns (uint224) { return ~b; }
131+
function solBWNot29UInt(uint232 b) external pure returns (uint232) { return ~b; }
132+
function solBWNot30UInt(uint240 b) external pure returns (uint240) { return ~b; }
133+
function solBWNot31UInt(uint248 b) external pure returns (uint248) { return ~b; }
134+
function solBWNot32UInt(uint256 b) external pure returns (uint256) { return ~b; }
135+
136+
/**
137+
for x in range(0,32):
138+
print(f"function solBWNot{x+1}Int(int{8*(x+1)} b) external pure returns (int{8*(x+1)})" + " { return ~b; }")
139+
*/
140+
function solBWNot1Int(int8 b) external pure returns (int8) { return ~b; }
141+
function solBWNot2Int(int16 b) external pure returns (int16) { return ~b; }
142+
function solBWNot3Int(int24 b) external pure returns (int24) { return ~b; }
143+
function solBWNot4Int(int32 b) external pure returns (int32) { return ~b; }
144+
function solBWNot5Int(int40 b) external pure returns (int40) { return ~b; }
145+
function solBWNot6Int(int48 b) external pure returns (int48) { return ~b; }
146+
function solBWNot7Int(int56 b) external pure returns (int56) { return ~b; }
147+
function solBWNot8Int(int64 b) external pure returns (int64) { return ~b; }
148+
function solBWNot9Int(int72 b) external pure returns (int72) { return ~b; }
149+
function solBWNot10Int(int80 b) external pure returns (int80) { return ~b; }
150+
function solBWNot11Int(int88 b) external pure returns (int88) { return ~b; }
151+
function solBWNot12Int(int96 b) external pure returns (int96) { return ~b; }
152+
function solBWNot13Int(int104 b) external pure returns (int104) { return ~b; }
153+
function solBWNot14Int(int112 b) external pure returns (int112) { return ~b; }
154+
function solBWNot15Int(int120 b) external pure returns (int120) { return ~b; }
155+
function solBWNot16Int(int128 b) external pure returns (int128) { return ~b; }
156+
function solBWNot17Int(int136 b) external pure returns (int136) { return ~b; }
157+
function solBWNot18Int(int144 b) external pure returns (int144) { return ~b; }
158+
function solBWNot19Int(int152 b) external pure returns (int152) { return ~b; }
159+
function solBWNot20Int(int160 b) external pure returns (int160) { return ~b; }
160+
function solBWNot21Int(int168 b) external pure returns (int168) { return ~b; }
161+
function solBWNot22Int(int176 b) external pure returns (int176) { return ~b; }
162+
function solBWNot23Int(int184 b) external pure returns (int184) { return ~b; }
163+
function solBWNot24Int(int192 b) external pure returns (int192) { return ~b; }
164+
function solBWNot25Int(int200 b) external pure returns (int200) { return ~b; }
165+
function solBWNot26Int(int208 b) external pure returns (int208) { return ~b; }
166+
function solBWNot27Int(int216 b) external pure returns (int216) { return ~b; }
167+
function solBWNot28Int(int224 b) external pure returns (int224) { return ~b; }
168+
function solBWNot29Int(int232 b) external pure returns (int232) { return ~b; }
169+
function solBWNot30Int(int240 b) external pure returns (int240) { return ~b; }
170+
function solBWNot31Int(int248 b) external pure returns (int248) { return ~b; }
171+
function solBWNot32Int(int256 b) external pure returns (int256) { return ~b; }
172+
}

‎Public/TestEVM/CVLCompilation/BWNot/Default.conf‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{
2+
"files": [
3+
"C.sol"
4+
],
5+
"solc": "solc8.19",
6+
"verify": "C:c.spec"
7+
8+
}

0 commit comments

Comments
 (0)