diff --git a/testcases/automatic/usage-check-1.occ.test b/testcases/automatic/usage-check-1.occ.test index e558c2b..fc0197e 100644 --- a/testcases/automatic/usage-check-1.occ.test +++ b/testcases/automatic/usage-check-1.occ.test @@ -22,10 +22,20 @@ PROC m() a[0] := 3 a[0] := 4 +%FAIL Identical constants, PAR assign + a[0],a[0] := 3,4 + %PASS Same constant, different array a[0] := 3 b[0] := 4 +%FAIL Identical variables + x := 3 + x := 4 + +%FAIL Identical variables, PAR assign + x,x := 3,4 + %FAIL Variable and a constant a[0] := 3 a[x] := 4 diff --git a/testcases/automatic/usage-check-3.occ.test b/testcases/automatic/usage-check-3.occ.test new file mode 100644 index 0000000..7804881 --- /dev/null +++ b/testcases/automatic/usage-check-3.occ.test @@ -0,0 +1,33 @@ +-- This file tests simple array uses without replication +-- Four unknown variables are available; x, y, z. +-- Two arrays are automatically declared; a (size 10) and b (size 12) + +PROC p(INT x, y, z) + [10]INT a: + [12]INT b: +%% +: + +PROC m() + SKIP +: + +%FAIL same items in SEQ replicator + SEQ i = 0 FOR 6 + PAR + a[i] := 3 + a[i] := 4 + +%FAIL Modulo items in SEQ replicator (unsafe) + SEQ i = 0 FOR 6 + PAR + a[(i + 1) REM 4] := 3 + a[i] := 4 + +%PASS Modulo items in SEQ replicator (safe) + SEQ i = 0 FOR 6 + PAR + a[(i + 1) REM 5] := 3 + a[i] := 4 + +% diff --git a/transformations/ArrayUsageCheckTest.hs b/transformations/ArrayUsageCheckTest.hs index 89130c9..2978264 100644 --- a/transformations/ArrayUsageCheckTest.hs +++ b/transformations/ArrayUsageCheckTest.hs @@ -767,6 +767,7 @@ ioqcTests :: IO (Test, [QuickCheckTest]) ioqcTests = do usageCheckTest1 <- automaticTest "testcases/automatic/usage-check-1.occ.test" usageCheckTest2 <- automaticTest "testcases/automatic/usage-check-2.occ.test" + usageCheckTest3 <- automaticTest "testcases/automatic/usage-check-3.occ.test" return (TestList [ @@ -775,6 +776,7 @@ ioqcTests ,testMakeEquations ,usageCheckTest1 ,usageCheckTest2 + ,usageCheckTest3 ] ,qcOmegaEquality ++ qcOmegaPrune)