/* Special tests for the Call rules. To be run with call-contract.txt */

// Check that the storage can have the right values before calling (at this point there is only one possible value at call level 0)
test storageSoundnesBeforeTest expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
		stackMoreAbstractThanForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))),
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 

test storagePrecisePossibleBeforeTest expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
		stackEqualForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
		?mem = [@V(0)],
		(select ?stor 3) = @V(10);  

test storagePreciseUniqueBeforeTest expect UNSAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{7}(?size, ?sa, ?mem, ?in, ?stor, false),
		(?size != 4 || ?mem != [@V(0)] 
		|| stackInequalExists{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)) 
		|| (select ?stor 3) != @V(10)); 

//Check for the right storage when reentering (can be 10 or 20, but nothing else)
test storageSoundnessReenteringTest1 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
		valueMoreAbstractThan(?in, @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 

test storageSoundnessReenteringTest2 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
		valueMoreAbstractThan(?in, @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 

test storagePrecisePossibleReenteringTest1 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
		?mem = [@V(0)], 
		?in = @T, 
		(select ?stor 3) = @V(10);  

test storagePrecisePossibleReenteringTest2 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
		?mem = [@V(0)],
		?in = @T,
		(select ?stor 3) = @V(20); 

test storagePreciseUniqueReenteringTest expect UNSAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{0}(?size, ?sa, ?mem, ?in, ?stor, true),
		(?mem != [@V(0)] || ?in != @T || ?size != 0 || 
		(select ?stor 3) != @V(10) && (select ?stor 3) != @V(20)); 

// Check that the storage is sound after reentering (on both levels)
test storageSoundnessResumeTest1 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 

test storageSoundnessResumeTest2 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 

test storageSoundnessResumeTest3 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 

test storageSoundnessResumeTest4 expect SAT 
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 

// Check that the storage is right when halting
test storageSoundnessHaltTest1 expect SAT 
	[?res: AbsDom, ?stor: array<AbsDom>]
	Halt(?stor, ?res, false), 
	valueMoreAbstractThan(?res, @V(0)),
	arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));

test storageSoundnessHaltTest2 expect SAT 
	[?res: AbsDom, ?stor: array<AbsDom>]
	Halt(?stor, ?res, true),
	valueMoreAbstractThan(?res, @V(0)), 
	arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));

test storagePrecisePossibleHaltTest1 expect SAT 
	[?res: AbsDom, ?stor: array<AbsDom>]
	Halt(?stor, ?res, false),
	?res = @V(0), 
	(select ?stor 3) = @V(20);

test storagePrecisePossibleHaltTest2 expect SAT 
	[?res: AbsDom, ?stor: array<AbsDom>]
	Halt(?stor, ?res, true),
	?res = @V(0),  
	(select ?stor 3) = @V(20);

test storagePreciseUniqueHaltTest expect UNSAT 
	[?res: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
	Halt(?stor, ?res, ?cl), 
	(select ?stor 3) != @V(20) || (?res != @V(0)) ;