blob: 6a94df739ed3b24e4237771af7c6b0ca362df9c1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Basetypes;
using System.Diagnostics;
namespace GPUVerify
{
class ReadCollector : AccessCollector
{
public List<AccessRecord> accesses = new List<AccessRecord>();
public ReadCollector(IKernelArrayInfo NonLocalState)
: base(NonLocalState)
{
}
public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
{
return node;
}
public override Expr VisitNAryExpr(NAryExpr node)
{
if (node.Fun is MapSelect)
{
if ((node.Fun as MapSelect).Arity > 1)
{
MultiDimensionalMapError();
}
Debug.Assert(node.Args[0] is IdentifierExpr);
var ReadVariable = (node.Args[0] as IdentifierExpr).Decl;
var Index = node.Args[1];
this.VisitExpr(node.Args[1]);
if (NonLocalState.Contains(ReadVariable))
{
accesses.Add(new AccessRecord(ReadVariable, Index));
}
return node;
}
else
{
return base.VisitNAryExpr(node);
}
}
}
}
|
