2141 Commits (43ee4e8179b024375f51461b9d8e1ed50b0e8c0a)

 

All Branches   

Search

Author	SHA1	Message	Date
Bernhard Mueller	43ee4e8179	Fix z3 version	6 years ago
Bernhard Mueller	9c92f1b24c	Fix z3 version	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
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
Nathan	0290de26f8	remove caller and call_value constraints from concretization logic	6 years ago
Nathan	e3386bcf98	output transaction sequence as verbose output	6 years ago
Dr. Sergey Pogodin	e260db5056	Another fix of the docker build & release script	6 years ago
Dr. Sergey Pogodin	aeefb7416e	A misprint fix	6 years ago
Dr. Sergey Pogodin	5f8d7382ef	Fix of Docker build & release shell scrip	6 years ago
Dr. Sergey Pogodin	450a1be06c	Temporary disables tests requirement for DockerHub "mythril/myth-dev" release	6 years ago
Dr. Sergey Pogodin	6e4ace9f73	Automatic releases of "develop" to "mythril/myth-dev" DockerHub container	6 years ago
Bernhard Mueller	405f26fab8	Merge pull request #636 from JoranHonig/bugfix/633_reentrancy ... Bugfix 633 State change after external call	6 years ago
Joran Honig	c6a0644c46	fix missing call variable	6 years ago
Joran Honig	bde69593f4	Don't check for requires as this results in false negatives	6 years ago
Joran Honig	31a8107daf	Make search_children compatible with multi transactional analysis	6 years ago
Joran Honig	f6749a1e97	Bugfix search_children	6 years ago
Joran Honig	9846019ab5	black fixes	6 years ago
Joran Honig	a83936a94c	Fix missing import and style	6 years ago
Joran Honig	06f92f64cd	remove unintended ouputs current	6 years ago
Joran Honig	9fe0964f35	merge fixes	6 years ago
Joran Honig	c8e4aef7cd	Merge remote-tracking branch 'upstream/master' into merge_master	6 years ago
Nathan	7cc4d6cdee	absolutely nothing	6 years ago
Bernhard Mueller	f66d5f4c89	Merge pull request #619 from nbanmp/transaction_sequence ... Concrete transaction sequence generation	6 years ago
Bernhard Mueller	67660ab7e0	Merge branch 'develop' into transaction_sequence	6 years ago