From eb2b6fda659fda09be89e4360eada2f123a3c80c Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Fri, 15 Jun 2012 20:57:11 +0100
Subject: GPUVerify: implement is-a-constant analysis

This analysis is used to generate race checking invariants for
arbitrary (thread-level) constant offsets, in place of invariant
generators for four specific constants (thread-id, global-id, 2D
thread-id and 2D global-id) which are subsumed by the new analysis.
The main motivation is to be able to recognise offsets used by
word level accesses into byte arrays, which are formed from linear
combinations of thread IDs and constants.

This change allows us to remove the 2D and global size analyses,
resulting in a 536-line net reduction in total code size.
---
 Source/Core/Util.cs | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Source/Core/Util.cs')

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index f45e2995..a8e12f63 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -61,6 +61,11 @@ namespace Microsoft.Boogie {
     {
       foreach (var e in coll) fn(e);
     }
+
+    public static IEnumerable<Tuple<TSource1, TSource2>> Zip<TSource1, TSource2>(this IEnumerable<TSource1> source1, IEnumerable<TSource2> source2)
+    {
+      return source1.Zip(source2, (e1, e2) => new Tuple<TSource1, TSource2>(e1, e2));
+    }
   }
 
   public class TokenTextWriter : IDisposable {
-- 
cgit v1.2.3