chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							e08f521b7e
							
						
					 | 
					
						
						
							
							Merge pull request #6764 from ethereum/smt_fix_tuple_ice
						
						
						
						
						
						
						
						[SMTChecker] Fix ICE in unsupported function calls with multi return values 
						
					 | 
					
						2019-05-20 15:18:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							60a4f03d3d
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ice in unsupported functions with multi return values
						
						
						
						
						
					 | 
					
						2019-05-16 18:23:42 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							5493a41842
							
						
					 | 
					
						
						
							
							[SMTChecker] Move global variables and functions to encoding context
						
						
						
						
						
					 | 
					
						2019-05-16 18:11:31 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							4e430ba0ae
							
						
					 | 
					
						
						
							
							[SMTChecker] Move expression handling to EncodingContext
						
						
						
						
						
					 | 
					
						2019-05-14 15:56:43 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ebbe03cad6
							
						
					 | 
					
						
						
							
							[SMTChecker] Move variable handling to EncodingContext
						
						
						
						
						
					 | 
					
						2019-05-13 16:59:28 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							01dd9ba2ae
							
						
					 | 
					
						
						
							
							Merge pull request #6717 from ethereum/smt_namespace
						
						
						
						
						
						
						
						Move SMT specific code into smt namespace 
						
					 | 
					
						2019-05-13 12:45:34 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							e5d46767f1
							
						
					 | 
					
						
						
							
							Merge pull request #6722 from ethereum/smt_fix_variable_usage
						
						
						
						
						
						
						
						[SMTChecker] Fix VariableUsage for IndexAccess 
						
					 | 
					
						2019-05-13 10:17:26 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							fac383a233
							
						
					 | 
					
						
						
							
							Move SMT specific code into smt namespace
						
						
						
						
						
					 | 
					
						2019-05-10 20:03:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							cc40e65a4b
							
						
					 | 
					
						
						
							
							Merge pull request #6712 from ethereum/smt_unique_ptr
						
						
						
						
						
						
						
						[SMTChecker] Use unique_ptr instead of shared_ptr where applicable 
						
					 | 
					
						2019-05-10 12:53:53 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3ea5c112d3
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix VariableUsage for IndexAccess
						
						
						
						
						
					 | 
					
						2019-05-10 11:28:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							8d65fd18fc
							
						
					 | 
					
						
						
							
							[SMTChecker] Style changes
						
						
						
						
						
					 | 
					
						2019-05-09 19:15:43 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							89700dbcff
							
						
					 | 
					
						
						
							
							Merge pull request #6665 from ethereum/smt_inline_external_this
						
						
						
						
						
						
						
						[SMTChecker] Inline external function calls to `this` 
						
					 | 
					
						2019-05-09 19:09:08 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ef32bf185f
							
						
					 | 
					
						
						
							
							[SMTChecker] Inline external function calls to this.
						
						
						
						
						
					 | 
					
						2019-05-09 16:53:30 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							c8a017ccd6
							
						
					 | 
					
						
						
							
							[SMTChecker] Use unique_ptr instead of shared_ptr where applicable.
						
						
						
						
						
					 | 
					
						2019-05-09 16:34:22 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6027383ae5
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix call to function at state var init
						
						
						
						
						
					 | 
					
						2019-05-09 16:12:44 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3d52a6ca68
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in branch-inline function call-modify local variable
						
						
						
						
						
					 | 
					
						2019-05-09 09:15:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							9893cae27a
							
						
					 | 
					
						
						
							
							[SMTChecker] Make mergeVariables deterministic
						
						
						
						
						
					 | 
					
						2019-05-08 20:46:01 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							0b046897ae
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix unsupported type assignment
						
						
						
						
						
					 | 
					
						2019-05-08 14:28:23 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3c7540ceb2
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuples with multiple var decls
						
						
						
						
						
					 | 
					
						2019-05-07 16:57:27 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2139c20776
							
						
					 | 
					
						
						
							
							[SMTChecker] Support delete
						
						
						
						
						
					 | 
					
						2019-05-06 18:32:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							e99efec085
							
						
					 | 
					
						
						
							
							Merge pull request #6652 from ethereum/smt_tuple_function
						
						
						
						
						
						
						
						[SMTChecker] Support tuples as function calls with multiple return values 
						
					 | 
					
						2019-05-06 15:19:24 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							80712f44cb
							
						
					 | 
					
						
						
							
							Fix short circuit with assignments
						
						
						
						
						
					 | 
					
						2019-05-06 11:04:43 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							5440a53d4d
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuples as function calls with multiple return values
						
						
						
						
						
					 | 
					
						2019-05-03 06:10:22 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							204dcf1771
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuple assignments
						
						
						
						
						
					 | 
					
						2019-05-02 12:55:34 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6c7527ac90
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuple type declaration
						
						
						
						
						
					 | 
					
						2019-05-02 12:05:21 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							66655b87b0
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in fixed point operations
						
						
						
						
						
					 | 
					
						2019-05-02 10:59:23 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							dd4e938265
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in inherited state var
						
						
						
						
						
					 | 
					
						2019-05-02 10:03:12 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a6db37ac9c
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix bad cast in base constructor modifier.
						
						
						
						
						
					 | 
					
						2019-04-30 18:48:13 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e4989369d0
							
						
					 | 
					
						
						
							
							Refactor cast from identifier ref decl to var decl
						
						
						
						
						
					 | 
					
						2019-04-30 11:08:36 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							762f79f84d
							
						
					 | 
					
						
						
							
							Refactor assignment handling
						
						
						
						
						
					 | 
					
						2019-04-30 11:08:36 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							fc482de695
							
						
					 | 
					
						
						
							
							[SMTChecker] Support address members
						
						
						
						
						
					 | 
					
						2019-04-25 16:24:36 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							dd1afeba52
							
						
					 | 
					
						
						
							
							[SMTChecker] Support this as address
						
						
						
						
						
					 | 
					
						2019-04-18 17:56:52 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							03d18f1b98
							
						
					 | 
					
						
						
							
							[SMTChecker] Add note about not inlining external function calls
						
						
						
						
						
					 | 
					
						2019-04-17 16:14:07 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							721bf367a3
							
						
					 | 
					
						
						
							
							[libsolidity] TypeProvider: eliminate redundant "Type" suffix in provider function signatures.
						
						
						
						
						
					 | 
					
						2019-04-17 14:42:07 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							862b65d6e3
							
						
					 | 
					
						
						
							
							[libsolidity] remove ReferenceType::copyForLocationIfReference (use TypeProvider instead)
						
						
						
						
						
					 | 
					
						2019-04-17 13:25:03 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
						
						
							
						
						
							58a45f2cb6
							
						
					 | 
					
						
						
							
							[libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...).
						
						
						
						
						
					 | 
					
						2019-04-16 18:28:40 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
						
						
							
						
						
							bf43eebea9
							
						
					 | 
					
						
						
							
							libsolidity: Introducing TypeProvider API, for clear type system ownership.
						
						
						
						
						
					 | 
					
						2019-04-16 18:26:45 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							bf5792f7ca
							
						
					 | 
					
						
						
							
							Merge pull request #6483 from ethereum/smt_support_mod
						
						
						
						
						
						
						
						[SMTChecker] Support mod 
						
					 | 
					
						2019-04-15 13:42:18 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							73ac8f6220
							
						
					 | 
					
						
						
							
							Merge pull request #6421 from ethereum/smt_fix_variable_usage
						
						
						
						
						
						
						
						[SMTChecker] Refactor VariableUsage 
						
					 | 
					
						2019-04-15 13:39:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							af9f16e014
							
						
					 | 
					
						
						
							
							[SMTChecker] Support mod
						
						
						
						
						
					 | 
					
						2019-04-12 12:39:25 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							4fe303530a
							
						
					 | 
					
						
						
							
							[SMTChecker] Show unsupported warning for asm blocks
						
						
						
						
						
					 | 
					
						2019-04-05 16:41:15 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							79d8a4e13a
							
						
					 | 
					
						
						
							
							[SMTChecker] Refactor VariableUsage
						
						
						
						
						
					 | 
					
						2019-04-05 11:38:37 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							aa9b9aa87e
							
						
					 | 
					
						
						
							
							[SMTChecker] Support unary inc/dec for array/mapping access
						
						
						
						
						
					 | 
					
						2019-04-02 16:53:19 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							84251e5a22
							
						
					 | 
					
						
						
							
							Merge pull request #6405 from ethereum/smt_compound_assignment
						
						
						
						
						
						
						
						[SMTChecker] Support arithmetic compound assignment operators. 
						
					 | 
					
						2019-03-28 18:27:25 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a7e826a224
							
						
					 | 
					
						
						
							
							[SMTChecker] Implement short circuit
						
						
						
						
						
					 | 
					
						2019-03-28 16:08:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							15269067b5
							
						
					 | 
					
						
						
							
							Support arithmetic compound assignment operators
						
						
						
						
						
					 | 
					
						2019-03-28 15:27:52 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ecbf36f271
							
						
					 | 
					
						
						
							
							Refactor computing symbolic arithmetic operation
						
						
						
						
						
					 | 
					
						2019-03-28 15:27:36 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6f9b69ebc3
							
						
					 | 
					
						
						
							
							Refactor function that retrieves FunctionDefinition from FunctionCall
						
						
						
						
						
					 | 
					
						2019-03-28 14:32:47 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a207d7f44c
							
						
					 | 
					
						
						
							
							[SMTChecker] Add callstack model to overflow checks
						
						
						
						
						
					 | 
					
						2019-03-21 16:25:33 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							de89733bd6
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix nullptr deref
						
						
						
						
						
					 | 
					
						2019-03-21 15:46:54 +01:00 | 
					
					
						
						
							
							
							
						
					 |