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