Theory attributes

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

theory attributes
  imports "AutoCorres2.CTranslation"
begin

install_C_file "attributes.c"

ML ‹
local
open ProgramAnalysis
in
fun global_details vi = (srcname vi, length (get_attrs vi))

val all_global_details = get_globals #> map global_details
end
›

ML ‹
val results = CalculateState.get_csenv @{theory} "attributes.c"
  |> the
  |> all_global_details
  |> sort (prod_ord string_ord int_ord)
›

ML ‹
val _ = if results = [("u",1), ("v", 1)] then ()
        else error "Test case failure"
›

end