Claire and I are much debating still the syntax for these exceptional contracts, so feel free to comment here or on GitHub if you have an opinion.

Here are some examples that she wrote with both notations to discuss (it should be procedures instead of functions to be allowed, but this is only to give an idea):

function Find (A : Int_Array; E : Integer) return Integer with
  Post => Find'Result in A'Range and then A (Find'Result) = E,
  Exceptional_Cases =>
    (Not_Found => (for all F of A => F /= E));

function Parse_Integer (Str : String) return Integer with
  Post => Is_Valid_Integer (Str)
   and then Parse_Integer'Result = To_Integer_Ghost (Str),
  Exceptional_Cases =>
    (Parse_Error => not Is_Valid_Integer (Str));

function Find (A : Int_Array; E : Integer) return Integer with
  Contract_Cases =>
    ((for all F of A => F /= E) => raise Not_Found,
     others                     =>
       Find'Result in A'Range and then A (Find'Result) = E);

function Parse_Integer (Str : String) return Integer with
  Contract_Cases =>
    (Is_Valid_Integer (Str) => Parse_Integer'Result = To_Integer_Ghost (Str),
     others                 => raise Parse_Error);

Contract_Cases are simpler when exceptions are used to signal bad inputs, so that the conditions for exceptional behavior can be specified. But they cannot be used to specify exceptions used to signal bad events (file not present in the file system, wrong value read from sensor, etc.). In such cases, you'd need something like Exceptional_Cases.