Theory HeapWrap

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

(*
 * Simple test cases for heap_abs_syntax feature.
 * JIRA issue ID: VER-356
 *)
theory HeapWrap
imports "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file "heap_wrap.c"
autocorres [heap_abs_syntax] "heap_wrap.c"

context heap_wrap_all_impl begin
thm f1'_def f2'_def f3'_def f4'_def f5'_def f6'_def f7'_def f8'_def
end

context heap_wrap_simpl
begin

(* overloaded syntax is not scalable *)
term "s[p→right := s[q]→left][q]→right = s[r] +p uint (s[t]→x) ∧
      s[p→right := s[q]→left] = s[q→left := s[p]→right] ∧
      s[t]→p = s[q]→p ∧
      s[ptr_coerce (s[p]→p) :: 32 word ptr] = ucast (s[q]→x)"

end

end