cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
23,084 Commits 348 Branches 121 Tags 100 MiB
c2e2adb953
Commit Graph

61 Commits

Author SHA1 Message Date
Leo Alt
24df40de9a Allow running Eldarica from the command line 2022-11-22 21:16:45 +01:00
George Plotnikov
44a2dd864f Update CVC4::BitVector ctor call 2022-09-26 23:03:42 +02:00
Marenz
f7cc29bec1 Add std:: qualifier to move() calls 2022-08-30 11:12:15 +02:00
Christian Parpart
4ae43884d0 Apply a better way to annotate unreachability to the C++ compiler. 2022-06-07 16:41:04 +02:00
Kamil Śliwak
e19e6ad806 Remove empty assertion messages in a fews places 2022-06-01 20:37:48 +02:00
Kamil Śliwak
539e139555 Add explicit throws after some assertions to work around a spurious warning in GCC 12.1 2022-06-01 20:37:48 +02:00
Leo Alt
60b405aaa9 Support new z3 AST node 2022-05-12 10:50:30 +02:00
Kamil Śliwak
3c5930dd8e Put arguments in parantheses in assert macro definitions 2022-04-06 22:26:21 +02:00
Leo Alt
1d65977769 Adjust Z3Interface::fromZ3 for the extra cases 2021-10-26 11:30:30 +02:00
Leo Alt
9a87680d21 Add invariant to the solver results 2021-10-26 11:30:30 +02:00
Kamil Śliwak
7f7107405f Try out the new assertion macro variants with less arguments 2021-10-04 12:05:00 +02:00
Kamil Śliwak
0745842d46 Use BOOST_PP_OVERLOAD() to allow invoking the assertion macros without a message 2021-10-04 12:05:00 +02:00
Kamil Śliwak
4fe6aa1328 Add default messages to assertion macros 2021-10-04 12:05:00 +02:00
chriseth
1531863835 Split Common.h into Numeric.h. 2021-09-23 15:27:29 +02:00
Kamil Śliwak
b3a513d3b6 SMTSolverChoice: Rewrite operator & not to modify its argument 2021-09-17 21:39:29 +02:00
Kamil Śliwak
588ec39eef SMTSolverChoice: Make more members const/noexcept 2021-09-17 21:39:29 +02:00
Leo Alt
61160aa0e7 Add constraints correlating address(this).balance and msg.value 2021-08-25 21:10:08 +02:00
Leo Alt
6c8ecfa82c Add option to choose solver 2021-07-27 17:14:21 +02:00
Leo Alt
f7b045b886 review 2021-05-26 22:12:49 +02:00
Leo Alt
5c3b5f86f3 Fix 2's complement 2021-05-26 22:12:49 +02:00
Leo Alt
3a0358bfb7 Replace real division by integer division 2021-05-26 22:12:49 +02:00
Leo Alt
fdf4c1ed9a Replace negative number literals by (0 - literal) 2021-05-26 22:12:49 +02:00
Leo Alt
b57b8daf0a Replace implies by => 2021-05-26 22:12:49 +02:00
Leo Alt
daea5f886d Fix CHCSmtLib2Interface 2021-05-26 22:12:49 +02:00
Alex Beregszaszi
e39433198d Remove the usage of boost::noncopyable 
Prior to this half of the codebase used explicit deleted copy constructors, the others used boost::noncopyable.
 2021-04-23 14:57:01 +01:00
Martin Blicha
0340510c53 [SMTChecker] correct handling of FixedBytes constants initialized with string literal 2021-03-04 15:14:47 +01:00
Daniel Kirchner
7308abc084 Allow loading Z3 dynamically at runtime. 2020-12-10 16:47:47 +01:00
Alex Beregszaszi
7e88ba8da0 Enable the -Wconversion warning 2020-12-08 16:45:24 +00:00
Daniel Kirchner
cb72d76aaf Add const ref to prevent segfaults. 2020-12-04 14:57:46 +01:00
Leonardo Alt
4210e09d9a Do not request proof for old z3 2020-12-03 20:57:23 +01:00
a3d4
148c379ab9 Fix Visual Studio compilation error (add missing include <optional>) 2020-11-16 17:42:51 +01:00
Alex Beregszaszi
2f899bbffa [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
Leonardo Alt
d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Leonardo Alt
446e46fe06 Use Expression instead of plain strings for counterexamples 2020-10-27 12:04:51 +00:00
Leonardo Alt
72b052eae7 Convert z3::expr to smtutil::Expression 2020-10-27 12:04:51 +00:00
Leonardo Alt
0223571987 [SMTChecker] Do not report error when rlimit 2020-09-25 18:43:10 +02:00
Leonardo
35a7d5d3e4
Merge pull request #9873 from ethereum/smt_dec_rlimit 
[SMTChecker] Decrease rlimit
 2020-09-23 23:11:59 +02:00
Leonardo Alt
ebb6f61506 [SMTChecker] Decrease rlimit 2020-09-23 19:28:47 +02:00
Leonardo Alt
5917fd82b3 [SMTChecker] Do not throw when counterexample is not available (older z3 versions) 2020-09-23 19:17:38 +02:00
chriseth
6e2d2feb10 Small fixes wrt ReasoningBasedSimplifier. 2020-09-16 18:08:54 +02:00
chriseth
f73fb726af Reasoning based optimizer. 2020-09-15 15:57:58 +02:00
Leonardo Alt
23ee011c56 [SMTChecker] Fix imports 2020-09-11 13:34:46 +02:00
Leonardo Alt
40197df104 [SMTChecker] Support shifts 2020-09-09 19:47:52 +02:00
chriseth
a2cac93cbf Introduce bitvector sort. 2020-09-09 17:26:52 +02:00
Leonardo Alt
7ca335adde Decrease rlimit 2020-09-01 08:25:07 +02:00
Djordje Mijovic
11a7763f49 [SMTChecker] Support bitwise or, xor and not. 2020-08-26 11:06:56 +02:00
Leonardo Alt
5bb4e73693 Review 1 2020-07-23 18:49:03 +02:00
Leonardo Alt
51721c3080 Double SAT run for cex 2020-07-23 18:49:03 +02:00
Leonardo Alt
744905525f Convert z3 cex graph into STL 2020-07-23 18:49:03 +02:00
Sachin Grover
b7adb2aa42 Add SPDX license identifier if not present already in source file 
Fixes: #9220
 2020-07-17 20:24:12 +05:30