GPUVerify: refactor candidate invariant generators and analyses to use regions

The main goal of this change is to make the candidate invariant
generation code and various analyses capable of handling both
structured and unstructured programs.  This is achieved using a
high level abstraction of "regions" -- a region may either be a
"root region" representing the entire implementation, or a natural
loop within that implementation.  Note that this is a subset to the
term's meaning in the context of compilers, in which regions are also
used for conditional control flow.  Each region consists of a set of
commands and a set of child regions.

This change also has the side effect of eliminating a large amount of
boilerplate code -- its net effect is to reduce the number of lines
of code by 88.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index 73f038fb..d38c57af 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -9,7 +9,7 @@ namespace GPUVerify
     class NullRaceInstrumenter : IRaceInstrumenter

     {

 

-        public void AddRaceCheckingCandidateInvariants(Implementation impl, Microsoft.Boogie.WhileCmd wc)

+        public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)

         {

             

         }