Elementwise encoding.

Increase group size to N. Then we can instantiate the endproof so that we can
prove: t < t' ==> r[t] + l[t] <= r[t'].

The following should be equivalent but has problems in translation through the
frontend (x and y get split into multiple variables which are each separately
havoced):

  dtype x, y;
  __assume(iselement(x));
  __assume(iselement(y));
  __barrier_invariant(final_upsweep_barrier(tid,ghostsum,len), upsweep_instantiation*);
  __barrier_invariant(final_downsweep_barrier(tid,result,ghostsum), x2t(x), x2t(y));
  barrier(CLK_LOCAL_MEM_FENCE);
  __non_temporal(__assert(__implies(x < y, raddf(result[x], len[x]) <= result[y])));

  * upsweep_instantiation is same as instantiation for SPEC_ELEMENTWISE with
  s/tid/x and s/tid'/y.
Merge branch 'master' of github.com:nchong/barrier-reasoning-tests
Fix problems when verifying full kernel.

Originally I wanted to follow something like the --delay-nooverflow switch of
genscan.py. This delays the introduction of the unsound nooverflow predicate
until it is needed, which is right at the endproof. Unfortunately, this is a
little tricky because it does not really follow proper barrier invariant
semantics. At the last barrier we prove the final upsweep/downsweep invariants
which do *not* include the nooverflow predicates but assume/instantiate the
invariants *with* the nooverflow predicates.

So here's what currently happens with the OpenCL kernel:
-DINC_UPSWEEP by itself
will omit the nooverflow predicate in the upsweep invariant

-DINC_DOWNSWEEP by itself
will omit the nooverflow predicate in the downsweep invariant

-DINC_ENDSPEC by itself
will include the nooverflow predicate in the final upsweep/downsweep invariants

-DINC_UPSWEEP -DINC_DOWNSWEEP
will omit the nooverflow predicate in the upsweep/downsweep invariants

-DINC_UPSWEEP -DINC_DOWNSWEEP -DINC_ENDSPEC
will include the nooverflow predicate everywhere

(there are other switch combinations but they are not as interesting at these
 ones)

The final thing to say is that the GPUVerify frontend can be made to work with
different rtypes but you have to change the function prototype of
__add_noovfl_unsigned().