diff --git a/checks/ArrayUsageCheckTest.hs b/checks/ArrayUsageCheckTest.hs index 03533b1..9682f9b 100644 --- a/checks/ArrayUsageCheckTest.hs +++ b/checks/ArrayUsageCheckTest.hs @@ -1172,6 +1172,7 @@ ioqcTests ,"testcases/automatic/usage-check-3.occ.test" ,"testcases/automatic/usage-check-4.occ.test" ,"testcases/automatic/usage-check-5.occ.test" + , "testcases/automatic/usage-check-6.occ.test" ] ,return $ qcOmegaEquality ++ qcOmegaPrune ++ qcTestMakeEquations) diff --git a/testcases/automatic/usage-check-6.occ.test b/testcases/automatic/usage-check-6.occ.test new file mode 100644 index 0000000..87f85dd --- /dev/null +++ b/testcases/automatic/usage-check-6.occ.test @@ -0,0 +1,32 @@ +-- This file tests array uses with prior knowledge + +PROC p(INT x, y, z) + INT i,j: + [10]INT a: +%% +: + +PROC m() + SKIP +: + +%PASS Distinct variables + SEQ + i, j := 1,2 + PAR + a[i] := 0 + a[j] := 0 +%FAIL Same variable + SEQ + i, j := 1, 1 + PAR + a[i] := 0 + a[j] := 0 +%PASS Distinct variable based on earlier equality + SEQ + i := j + PAR + a[i] := 0 + a[j + 1] := 0 + +%