mirror of
				https://github.com/ethereum/solidity
				synced 2023-10-03 13:03:40 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			42 lines
		
	
	
		
			876 B
		
	
	
	
		
			Solidity
		
	
	
	
	
	
			
		
		
	
	
			42 lines
		
	
	
		
			876 B
		
	
	
	
		
			Solidity
		
	
	
	
	
	
pragma experimental SMTChecker;
 | 
						|
 | 
						|
contract C
 | 
						|
{
 | 
						|
	uint x;
 | 
						|
	uint y;
 | 
						|
	uint z;
 | 
						|
 | 
						|
	function f() public {
 | 
						|
		if (x == 1)
 | 
						|
			x = 2;
 | 
						|
		else
 | 
						|
			x = 1;
 | 
						|
		g();
 | 
						|
		assert(y == 1);
 | 
						|
	}
 | 
						|
 | 
						|
	function g() public {
 | 
						|
		y = 1;
 | 
						|
		h();
 | 
						|
		assert(z == 1);
 | 
						|
	}
 | 
						|
 | 
						|
	function h() public {
 | 
						|
		z = 1;
 | 
						|
		x = 1;
 | 
						|
		f();
 | 
						|
		// This fails for the following calls to the contract:
 | 
						|
		// h()
 | 
						|
		// g() h()
 | 
						|
		// It does not fail for f() g() h() because in that case
 | 
						|
		// h() will not inline f() since it already is in the callstack.
 | 
						|
		assert(x == 1);
 | 
						|
	}
 | 
						|
}
 | 
						|
// ----
 | 
						|
// Warning: (271-274): Assertion checker does not support recursive function calls.
 | 
						|
// Warning: (140-143): Assertion checker does not support recursive function calls.
 | 
						|
// Warning: (483-497): Assertion violation happens here
 | 
						|
// Warning: (201-204): Assertion checker does not support recursive function calls.
 | 
						|
// Warning: (483-497): Assertion violation happens here
 |