- Interval inference and typing
- Multi-dimensional arrays with ranges as indexes:
  - If the only range is the last index -> single call to builtin
  - Else -> not yet "arithmetic over set of pointers" (requires Mmodel modification)
- Tests for struct
- Richer pattern matching instead of is_trange
- has_range -> Misc.is_range_free
- Using Cil_const.make_logic_var_kind, Logic_const.taddrof, Logic_const.type_of_element and Logic_utils.mk_cast
- [elt] @ list -> elt :: list
- Options.fatal -> Options.abort
- Comments:
  - On the Range Elimination operation
  - Describing the formula for the range-free term
  - Describing mmodel_call_with_ranges and mmodel_call_default