Theory signedoverflow

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

theory signedoverflow
imports "AutoCorres2.CTranslation"
begin

install_C_file "signedoverflow.c"

context signedoverflow_simpl
begin

thm f_body_def

(* painful lemma about sint and word arithmetic results...
lemma j0: "Γ ⊢ ⦃ True ⦄ Call f_'proc ⦃ ´ret__int = 0 ⦄"
apply vcg
apply simp_all
apply auto
*)

thm g_body_def
end

lemma (in g_impl) "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL g(1) ⦃ ´ret' = - 1 ⦄"
apply vcg
apply (simp add: word_sle_def)
done

lemma (in g_impl) "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL g(- 2147483648) ⦃ ´ret' = - 1 ⦄"
apply vcg
apply (simp add: word_sle_def)
done

lemma (in g_impl) "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL g(- 2147483647) ⦃ ´ret' = 2147483647 ⦄"
apply vcg
apply (simp add: word_sle_def)
done

end (* theory *)