1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(* This is the "standard" instantiation of the MemoryModelExtras
12   signature.
13
14   Other implementations using the parser code may wish to 'use' a different
15   file than this one.  The theory is that everything will "just work" as
16   long as that file declares a structure MemoryModelExtras matching the
17   signature.
18*)
19
20structure MemoryModelExtras : MEMORY_MODEL_EXTRAS =
21struct
22
23open TermsTypes UMM_TermsTypes
24val extended_heap_ty = heap_raw_ty
25fun check_safety {heap=h,ptrval} = let
26  val heap_desc = mk_hrs_htd_t $ h
27in
28  (mk_ptr_safe ptrval heap_desc, safety_error)
29end
30
31fun dereference_ptr {heap,ptrval} = mk_lift(mk_hrs_mem_t $ heap,ptrval)
32
33fun mk_heap_update_extended t = mk_hrs_mem_update_t $ t
34
35fun mk_aux_guard t = mk_aux_guard_t $ t
36
37fun mk_aux_update t = mk_hrs_htd_update_t $ (mk_aux_heap_desc_t $ t)
38
39fun mk_aux_type ty = mk_auxupd_ty ty
40
41val check_global_record_type = HeapStateType.hst_prove_globals
42
43fun mk_lookup_proc_pair symtab naming addr = let
44  val argTs = [fastype_of symtab, fastype_of naming, fastype_of addr]
45  in (Const (@{const_name lookup_proc}, argTs ---> int)
46        $ symtab $ naming $ addr,
47    Const (@{const_name lookup_proc_safe}, argTs ---> HOLogic.boolT)
48        $ symtab $ naming $ addr)
49  end
50
51structure UserTypeDeclChecking =
52struct
53  open UMM_Proofs
54  type t = T
55  type csenv = ProgramAnalysis.csenv
56  val initial_state = umm_empty_state
57  val finalise = umm_finalise
58  fun struct_type _ {struct_type,state} thy =
59      umm_struct_calculation (struct_type,state,thy)
60  fun array_type _ {element_type, array_size, state} thy =
61      umm_array_calculation element_type array_size state thy
62
63end
64
65end
66