Add LocalVar<T> class

This allows for the type-safe handling of thread-local and shared
variable accesses. The following changes support this type safety:

* Add LiteralReadInstr<T*> specialization for pointers as uintptr_t
* Create type-strong return type for Recorder::instr() write events
* Allow intermixing of ReadInstr<T> pointers as operands in binary
  operators.
Strengthen LocalVar<T> tests
Add SharedVar<T> class
Support rvalue reference as operands

Allow instructions such as "buffer[2]+'A'" where buffer is a char[].
Fix typo in variable name
Support fixed-size array initialization

These changes fixed-size arrays to be directly written. These direct
writes are encoded as constant arrays filled with a given expression.
The following changes were required for this:

* Add Z3::create_array_constant()
* Add LiteralReadInstr<T[N]>::element_literal()
* Add Z3ReadEncoder::encode(const LiteralReadInstr<T[N]>&)
* Add private Event(id, ...) and ReadEvent<T>(id, ...) constructors
* Add internal_make_read_event() to bypass read event ID control
Add functional tests for symbolic concurrency analysis
Support assignment of array dereferences to scalar
Create data structure for series-parallel graphs

Create a doubly-linked binary tree structure that represents the
unrolled control flow graph of a program. Formally, this new data
structure is a directed acyclic series-parallel graph.
init_recorder() reinitializes all static counters
Handle consecutive and nested blocks

Create a recursive data structure for the control flow unit in
structured program.
Use doubly-linked list to sequence blocks
Order events in forward_list according to program order

Since forward_list<T>::push_back() does not exist, we implement our own
using a constant iterator together with forward_list<T>::insert_after().
This implementation is O(1).
Encode multiple paths in a thread as partial orders

These changes unify the treatment of inter-thread and intra-thread
memory accesses. At the core of this unification is the representation
of a structured program as a series-parallel graph. This graph induces a
partial order between events in a single thread. This ordering together
with the other axioms allow us to encode multiple execution paths
within a single thread of execution thereby generalizing multi-path
(i.e. CBMC-style) symbolic execution to concurrent programs. Further
work and optimizations on thread-local events, however, is required.
Add block header file