2175 Commits (38ee8c452396a885ca94abf1c9955283e50160af)

 

All Branches   

Search

Author	SHA1	Message	Date
JoranHonig	38ee8c4523	Merge branch 'develop' into feature/type-hints-develop	6 years ago
Nikhil Parasaram	47bf8a5ee8	Merge pull request #653 from ConsenSys/hotfix/solc-version-binary ... Hotfix/solc version binary	6 years ago
Dominik Muhs	ee9f3bd5e7	Apply black	6 years ago
Dominik Muhs	027db3fb10	Replace specific Z3 hints with broader ExprRef	6 years ago
Dominik Muhs	856147c5b1	Fix type hint for LaserEVM.accounts	6 years ago
Dominik Muhs	50fbf29c90	Apply black	6 years ago
Dominik Muhs	a144c5a50d	Fix __getitem__ signature hints	6 years ago
Dominik Muhs	5167274644	Fix SVM init type signature	6 years ago
Dominik Muhs	76795763d2	Fix ecrecover type signature	6 years ago
Dominik Muhs	c3f80adfb6	Fix BitVecRef type hints	6 years ago
Dominik Muhs	8add0a7c58	Fix Calldata type hints	6 years ago
Dominik Muhs	e94ff999a1	Merge latest develop branch	6 years ago
Nikhil Parasaram	3470c89661	Merge branch 'develop' into hotfix/solc-version-binary	6 years ago
Bernhard Mueller	036278502a	Update version.py	6 years ago
JoranHonig	58c019ace4	Merge pull request #656 from ConsenSys/hotfix/revertoverflow ... revert changes to support z3 4.5	6 years ago
Joran Honig	9cbf1d55e5	revert changes to support z3 4.5	6 years ago
Bernhard Mueller	43ee4e8179	Fix z3 version	6 years ago
Bernhard Mueller	9c92f1b24c	Fix z3 version	6 years ago
Nikhil Parasaram	880b2bfcee	Merge branch 'develop' into hotfix/solc-version-binary	6 years ago
Nikhil Parasaram	e6f7423368	Merge pull request #648 from hzzhang/hzzhang/fix-bvmul-overflow-check ... analysis/integer: fix the overflow check of bit vector multiplication	6 years ago
JoranHonig	cb71b479e3	Merge branch 'develop' into hzzhang/fix-bvmul-overflow-check	6 years ago
JoranHonig	9e291734d6	Merge pull request #644 from hzzhang/hzzhang/misc-cleanup-and-fix ... Minor cleanup and fixes	6 years ago
JoranHonig	a0f9af540a	Merge branch 'develop' into hzzhang/fix-bvmul-overflow-check	6 years ago
Nikhil Parasaram	973148db66	Reformat code with black	6 years ago
Nikhil Parasaram	9dcfe53da0	Merge branch 'develop' of github.com:ConsenSys/mythril into hotfix/solc-version-binary	6 years ago
Nikhil Parasaram	9ee0014a1b	Pass solc binary to other functions	6 years ago
JoranHonig	26cbdafe67	Merge branch 'develop' into hzzhang/misc-cleanup-and-fix	6 years ago
Nikhil Parasaram	412e5bb3f9	Merge pull request #650 from ConsenSys/hotfix/variable_name ... fix missing call variable	6 years ago
Haozhong Zhang	a982a7d7fd	analysis/integer: switch addition overflow check to dedicated Z3 API ... Use Z3 API BVAddNoOverflow() in the constraint to check the bit vector addition overflow.	6 years ago
Haozhong Zhang	ee674ff803	analysis/integer: fix the overflow check of bit vector multiplication ... Differently than the bit vector addition, an overflowed bit vector multiplication does not necessarily result in a value less than any of its operands (e.g., the multiplication of two 8-bit vectors 0x7 and 4 produces 0xC). Fix this issue by using Z3 BVMulNoOverflow in the overflow check of bit vector multiplication.	6 years ago
Haozhong Zhang	0d0d8e5ac3	dependencies: bump the minimal Z3 version to 4.8 ... Following commits will use overflow checking APIs that are only available in newer versions of Z3.	6 years ago
Nikhil Parasaram	90c193af9a	Merge branch 'develop' into hotfix/variable_name	6 years ago
JoranHonig	f9a6b83e09	Merge branch 'develop' into hzzhang/misc-cleanup-and-fix	6 years ago
JoranHonig	7e1f377df1	Merge pull request #649 from JoranHonig/bugfix/typo ... subtraction typo fix	6 years ago
JoranHonig	9558d80c11	Merge branch 'develop' into hzzhang/misc-cleanup-and-fix	6 years ago
Joran Honig	adeec0264f	subtraction typo fix	6 years ago
Dr. Sergey Pogodin	3dd205d648	Version bumped to 0.19.0	6 years ago
Dr. Sergey Pogodin	f85d24bcc1	Merge branch 'develop'	6 years ago
Dr. Sergey Pogodin	befac7f40a	Disables API integration tests in CircleCI config	6 years ago
Bernhard Mueller	e665e5f34e	Merge branch 'JoranHonig-merge_master' into develop	6 years ago
Bernhard Mueller	3020da9b83	Merge branch 'merge_master' of https://github.com/JoranHonig/mythril into JoranHonig-merge_master	6 years ago
Bernhard Mueller	8fea106cb7	Set max-transaction-count default to 1	6 years ago
Bernhard Mueller	1fcdec0966	Merge pull request #637 from JoranHonig/bugfix/634_requires ... Bugfix 634: Don't check for requires as this results in false negatives	6 years ago
Bernhard Mueller	d8ddcb46a9	Merge pull request #642 from nbanmp/output_tx_sequence ... Output transaction sequence in verbose output	6 years ago
Nathan	74a1a401d3	remove unhelpful log messages	6 years ago
Nathan	2af841027c	remove unneeded check	6 years ago
Haozhong Zhang	91015e63ba	analysis/integer: remove unnecessary deepcopy of constraints ... `solver.get_model()` has no way to mutate constraints passed to it, so the expensive deepcopy of constraints before calling `solver.get_model()`is unnecessary.	6 years ago
Haozhong Zhang	725bfec464	laser/instruction: simplify before checking by Z3 is_true() ... Z3 is_true() does not automatically consider `expr == expr` to be true, so `is_true(key_argument == index_argument)` in `sstore_()` will miss lots of positive conditions and then generate lots of unnecessary subsequent paths. Take the following contract for example ``` contract Foo { mapping(address => uint) public balances; function bar(address _to, uint256 _value) public { require(balances[_to] + _value >= balances[_to]); balances[_to] += _value; balances[_to] += _value; } ``` Before this commit, - 772 nodes/771 edges/8288 states are generated. After this commit, - only 237 nodes/236 edges/3204 states are generated.	6 years ago
Haozhong Zhang	ce4075b8df	laser/instruction: remove unused solver in sstore_()	6 years ago
Haozhong Zhang	0f8e9144a6	analysis/transaction_order_dependence: import missing `copy` module in transaction_order_dependence.py ... copy.deepcopy() is used in transaction_order_dependence.py, but the `copy` module is not imported.	6 years ago