1(* 2 * Copyright 2018, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 *) 12 13(* /*? macros.generated_file_notice() ?*/ *) 14 15open preamble basis /*- if me.type.control -*/ componentTheory /*- else -*/ connectorTheory /*- endif -*/ 16 17val _ = new_theory "camkesEnd"; 18 19val _ = translation_extends /*- if me.type.control -*/ "component" /*- else -*/ "connector" /*- endif -*/; 20 21val supervisor = process_topdecs ` 22 fun camkes_entry u = 23 let 24 val dummy = Component.pre_init (); 25 26 val raw_result = Word8Array.array 1 (Word8.fromInt 0); 27 val dummy = #(pre_init_interface_sync) "" raw_result; 28 val result = Word8.toInt (Word8Array.sub raw_result 0) = 0; 29 30 val dummy = if result then (Component.post_init ()) else (); 31 32 val dummy = if result then (#(post_init_interface_sync) "" raw_result) else (); 33 val result = Word8.toInt (Word8Array.sub raw_result 0) = 0; 34 35 /*- if me.type.control -*/ 36 val dummy = if result then (Component.run ()) else (); 37 /*- else -*/ 38 val dummy = if result then (Connector.run ()) else (); 39 /*- endif -*/ 40 in 41 () 42 end 43`; 44 45val _ = append_prog supervisor; 46 47val _ = export_theory (); 48