Name Changes
{{{
$local_start  --> $begin_local
$local_end    --> $end_local
$pathCondition --> $print_path_condition
$hidden --> $is_hidden
$assume_push --> $push_assumption
$assume_pop --> $pop_assumption
$read_set_push --> $push_reads
$write_set_push --> $push_writes
$read_set_pop --> $pop_reads
$write_set_pop --> $pop_writes
$read_set_peek --> $peek_reads
$write_set_peek --> $peek_writes
$atomic_f --> ?
$default_value --> $initialize
}}}


add doc for `$is_concrete_int` (`civlc.cvh`).

change def of `$choose_int` to:

{{{
$atomic_f int $choose_int(int n) {
  if ($is_concrete_int(n))
    return $choose_int_concrete(n);
  else {
    int x=0;
    for (; x<n-1; x++) {
      $choose {
        ;
        break;
      }
    }
    return x;
  }
}
}}}


Move functions from civlc.cvh to libraries...
{{{
is_derefable, hide, reveal, hidden: pointer.cvh
elaborate_domain: domain.cvh
}}}

`#pragma CIVL` --> `#pragma civl`  (OK?)

`\executes_when`: make it work for atomic_f functions?



Some functions do not appear in any header:
  `$scope_defined`
  `$proc_defined`

Note: `$proc_null` is defined in `PP2CivlcTokenCConverter.java`
from the preprocessor, `$proc_null` is just an IDENTIFIER.
This class converts identifiers to the proper token.

We should probably replaced these with a single primitive: `$defined`.

Language change: atomic/yield/depends:

Get rid of begin/end local funtions.

Change grammar to allow the following kinds of statements:
{{{
  $atomic stmt
  $yield stmt
  $depends_on (expr) stmt
}}}

Example:
{{{
$depends_on(expr) $atomic {
  A;
  $atomic {
    B;
    $yield {
      C // this code is outside of atomic
    }
    $depends_on(expr) ...;
  }
}
}}}

translation:
{{{
  $atomic S --> begin_atomic; S end_atomic;
  $yield S --> begin_yield; S end_yield;
}}}

semantics:
state:
{{{
  atomicStack: stack of {0,1}. (1=begin_atomic, 0=begin_yield), initially empty
}}}
transitions:
{{{
  begin_atomic:
    enabled when lock is free or I own it, and first statement after begin_atomic is enabled
    if I don't own lock, obtain lock
    if atomicStack.length >= max : error
    atomicStack.push(1)
  end_atomic:
    assert !atomicStack.isEmpty() && atomicStack.top==1
    atomicStack.pop()
    if atomicStack.isEmpty() || atomicStack.top==0, release lock
  begin_yield:
    enabled when true;
    if I own lock, release lock;
    if atomicStack.length >= max: error
    atomicStack.push(0);
  end_yield:
    enabled when atomicStack==01* => (lock.isFree && first stmt after yield is enabled);
    assert !atomicStack.isEmpty && atomicStack.top==0 
    atomicStack.pop()
    if !atomicStack.isEmpty && atomicStack.top==1, obtain lock
}}}

Language change:

  `$assuming`

  `$track (rs,ws) stmt`

  `$untrack stmt`