-- 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
%PASS Distinct variables due to bounds
  SEQ k = 0 FOR 4
    PAR
      a[4] := 0
      a[k] := 0
%FAIL Non-distinct variables due to bounds
  SEQ k = 0 FOR 4
    PAR
      a[3] := 0
      a[k] := 0
%PASS Distinct due to IF
  IF
    i = 3
      PAR
        a[i] := 0
        a[4] := 0
    TRUE
      SKIP
%FAIL Non-distinct despite IF
  IF
    i <= 4
      PAR
        a[i] := 0
        a[4] := 0
    TRUE
      SKIP
%PASS Distinct variables, passed to PROC
  PROC foo(INT x, INT y)
    x, y := y, x
  :
  SEQ
    i, j := 1, 2
    foo(i, j)
%PASS Distinct array variables, passed to PROC
  PROC foo(INT x, INT y)
    x, y := y, x
  :
  SEQ
    i, j := 1, 2
    foo(a[i], a[j])
%PASS Distinct array variables, used in assignment
  PROC foo(INT x, INT y)
    x, y := y, x
  :
  SEQ
    i, j := 1, 2
    a[i], a[j] := 3, 4
%PASS IF, safe over replication
  PAR k = 0 FOR 10
    IF
      k = 3
        PAR
          a[k] := 1
          a[k+1] := 2
      TRUE
        SKIP
%FAIL IF, unsafe over replication
  PAR k = 0 FOR 10
    IF
      k = 3
        a[2] := 1
      TRUE
        a[k] := 3
%PASS IF, safe indirectly over replication
  PAR k = 0 FOR 10
    IF
      k = 3
        a[0] := 1
      TRUE
        SKIP
%PASS IF, safe indirectly over replication 2
  PAR k = 0 FOR 10
    IF
      k = 3
        a[0] := 1
      k <> 0
        a[k] := 1
      TRUE
        SKIP
%PASS IF, safe indirectly over replication 2B
  PAR k = 0 FOR 10
    IF
      k = 3
        a[0] := 1
      k > 0
        a[k] := 1
      TRUE
        SKIP
%PASS IF, safe indirectly over replication 3
  PAR k = 0 FOR 9
    IF
      k = 0
        a[9] := 3
      TRUE
        a[k] := 3
%FAIL IF, unsafe indirectly over replication
  PAR k = 0 FOR 10
    IF
      k = 3
        a[0] := 1
      k = 0
        a[k] := 1
      TRUE
        SKIP
%PASS Replicated, with VAL abbrev of replicator
  PAR
    PAR k = 0 FOR 5
      VAL kay IS k + 5:
      a[kay] := 4
    a[4] := 3
%FAIL Replicated, with VAL abbrev of replicator (unsafe)
  PAR
    PAR k = 0 FOR 5
      VAL kay IS k + 5:
      a[kay] := 4
    a[5] := 3
%PASS Replicated, with VAL and normal abbrev of replicator
  PAR
    PAR k = 0 FOR 5
      VAL kayplus3 IS k + 3:
      INT kay:
      SEQ
        kay := kayplus3 - 3
        a[kay] := 4
    a[5] := 3
%FAIL Replicated, with VAL and normal abbrev of replicator (unsafe)
  PAR
    PAR k = 0 FOR 5
      VAL kayplus3 IS k + 4:
      INT kay:
      SEQ
        kay := kayplus3 - 3
        a[kay] := 4
    a[5] := 3

%PASS Replicated, with VAL and normal abbrev of replicator in IF
  PAR
    PAR k = 0 FOR 5
      VAL kayplus3 IS k + 3:
      INT kay:
      SEQ
        IF
          i > 65
            kay := kayplus3 - 3
          TRUE
            kay := kayplus3 - 4
        a[kay] := 4
    a[5] := 3
%FAIL Replicated, with VAL and normal abbrev of replicator in IF (unsafe)
  PAR
    PAR k = 0 FOR 5
      VAL kayplus3 IS k + 3:
      INT kay:
      SEQ
        IF
          i > 65
            kay := kayplus3 - 3
          TRUE
            kay := kayplus3 - 2
        a[kay] := 4
    a[5] := 3

%PASS Replicated, following TRUE branch
  PAR
    a[0] := 3
    PAR k = 0 FOR 10
      IF
        k = 0
          SKIP
        TRUE
          a[k] := 4
%FAIL Replicated, following TRUE branch (unsafe)
  PAR
    a[0] := 3
    PAR k = 0 FOR 10
      IF
        k = 1
          SKIP
        TRUE
          a[k] := 4
%PASS Replicated, following NOT with = branch
  PAR
    a[0] := 3
    PAR k = 0 FOR 10
      IF
        NOT (k = 0)
          a[k] := 4
        TRUE
          SKIP
%FAIL Replicated, following NOT with = branch (unsafe)
  PAR
    a[0] := 3
    PAR k = 0 FOR 10
      IF
        NOT (k = 0)
          SKIP
        TRUE
          a[k] := 4
%PASS Replicated, following TRUE branch with OR
  PAR
    a[0] := 3
    a[9] := 4
    PAR k = 0 FOR 10
      IF
        (k = 0) OR (k = 9)
          SKIP
        TRUE
          a[k] := 4
%PASS Replicated, following TRUE branch with NOT and AND
  PAR
    a[0] := 3
    a[9] := 4
    PAR k = 0 FOR 10
      IF
        NOT ((k <> 0) AND (k <> 9))
          SKIP
        TRUE
          a[k] := 4
%FAIL Replicated, following TRUE branch with bad AND
  PAR
    a[0] := 3
    a[9] := 4
    PAR k = 0 FOR 10
      IF
        (k = 0) AND (k = 9)
          SKIP
        TRUE
          a[k] := 4

        

%