(* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * Copyright (c) 2022 Apple Inc. All rights reserved. * * SPDX-License-Identifier: BSD-2-Clause *) section "Function Pointers" theory fnptr imports AutoCorres begin (* FIXME: what about a final-autocorres sanity check? We could take all the method_callers, determine which functions they might call (via type), And see if the choosen WA and TS abstraction actually match. *)