File ‹list_reverse.c›

/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

typedef unsigned long word_t;

/** FNSPEC reverse_spec:
  "Γ ⊢
    ⦃ (list zs ´i)⇗sep⇖ ⦄
      ´ret' :== PROC reverse(´i)
    ⦃ (list (rev zs) (Ptr (scast ´ret')))⇗sep⇖ ⦄"
*/

long reverse(word_t *i)
{
  word_t j = 0;

  while (i)
    /** INV: "⦃ ∃xs ys. (list xs ´i ∧⇧* list ys (Ptr ´j))⇗sep⇖ ∧ rev zs = (rev xs)@ys ⦄" */
  {
    word_t *k = (word_t*)*i;

    *i = j;
    j = (word_t)i;
    i = k;
  }

  return j;
}