Theory locvarfncall

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

theory locvarfncall
imports "AutoCorres2.CTranslation"
begin

install_C_file "locvarfncall.c"

thm something_body_def
thm something_else_body_def
thm another_body_def

 
lemma (in locvarfncall_global_addresses) includes something_variables 
    shows foo: "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL something() ⦃ ´ret' = 112 ⦄"
apply vcg
apply simp

done

lemma (in locvarfncall_global_addresses) includes something_else_variables 
  shows "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL something_else(4)
           ⦃ ´ret' = 50 ⦄"
apply vcg
apply simp
done

text ‹Note that there is no explicit distinctness for the local variables 
of different procedures. Quite the opposite, parameters and local variables are 
encoded positionally for each procedure.
However, the calling conventions encoded in SIMPL procedure calls maintain the expected
'stack semantics' and don't get into the way even when procedures are inlined.
›


lemma (in locvarfncall_global_addresses) includes another_variables
  shows "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL another(4)
           ⦃ ´ret' = 51 ⦄"
apply vcg
apply simp
done

end