adds support for ternary operator (expr) ? expr : expr
enables writing Viper functions in Pancake annotations:
/* @ function sum(heap: IArray, base: Int, len: Int): Int
requires base >= 0 && len >= 0
requires base + len <= alen(heap)
requires forall i: Int :: base <= i && i < base + len ==> acc(heap[i], read)
{
(len == 0) ? 0 : (heap[base + len - 1] + sum(heap, base, len - 1))
} @*/
enables writing pre- and postconditions for ffi calls by specifying abstract Viper methods:
(expr) ? expr : expr