# .args. -contracts:none

# adapted from 150-require-ensure-lone-ident.cobra

# This test will probably break when Cobra starts statically analyzing contracts, but I guess that's a ways off.

class Test

	invariant
		.number > 0

	var _number as int

	get number from var

	def foo(s as String?) as String?
		require
			s and s.length
		ensure
			result
		body
			return s

	def bar(x as int) as int
		require
			x
		ensure
			result
		body
			return x - 1

	def baz
		.foo('aoeu')
#		expect RequireException
		.foo('')
#		expect RequireException
		.foo(nil)

		.bar(5)
#		expect RequireException
		.bar(0)
#		expect EnsureException
		.bar(1)

	def main is shared
		Test().baz