Theory fnptr_large_array

(*
 * Copyright (c) 2023 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory fnptr_large_array
  imports 
    AutoCorres2_Main.AutoCorres_Main
begin

install_C_file "fnptr_large_array.c"

autocorres fnptr_large_array.c
text ‹›
  ― ‹optimized performance of ‹AutoCorresUtil.dyn_call_split_simp_sidecondition_tac› with 
  @{ML Array_Selectors.array_selectors} enabled by default in @{command install_C_file}: takes about 60s›

end