2ecd91e36f
This allows us to check situations like this:
PAR i = 0 FOR 10
IF
i = 0
a[10] := 3
TRUE
a[i] := 3
Previously this would have been flagged unsafe (because 10 can overlap with 10 between the replicated branches).
But with this change, the equations on the replicators (including: i'>=i+1, i = 0, i' = 0) are included alongside 10=10, so there is no solution over all because the replicator equations prevent a solution (i.e. the 10 can't be used twice in parallel).
128 lines
2.0 KiB
Plaintext
128 lines
2.0 KiB
Plaintext
-- 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 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
|
|
|
|
%
|