/seL4-l4v-master/seL4/src/object/ |
H A D | schedcontrol.c | 13 static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t core, ticks_t budget, argument 17 target->scBadge = badge; 20 if (target->scTcb) { 22 SMP_COND_STATEMENT(remoteTCBStall(target->scTcb)); 24 tcbReleaseRemove(target->scTcb); 25 tcbSchedDequeue(target->scTcb); 27 if (NODE_STATE_ON_CORE(ksCurSC, target->scCore) == target) { 29 if (target->scCore == getCurrentCPUIndex()) { 38 chargeBudget(NODE_STATE_ON_CORE(ksConsumed, target [all...] |
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | encodeLib.sml | 60 fun target_bottom_value target bottom_target t = 64 val b2 = inst (map (fn t => t |-> target) types) b1 66 subst [mk_arb target |-> bottom_target] b2 148 (* Given the target type, each conv rewrites to convert a term given to *) 171 fun get_gen_type opr target t = 172 foldr (fn (x,t) => (opr (x,target)) --> t) (opr (t,target)) 175 fun get_encode_type target t = get_gen_type op--> target t 177 fun get_decode_type target 732 val target = (type_of o rand o lhs o snd o strip_forall o hd) clauses value 1475 val target = type_of term value 1507 val target = type_of (rand term) value 1550 let val target = type_of (rand term) value [all...] |
H A D | functionEncodeLib.sml | 116 (* a) (encode : t -> target) x where encode is a valid encoder *) 117 (* b) (f : t -> target) x where target is a known translation *) 129 val target = type_of term value 130 val enc = get_encode_function target t 134 (is_vartype target orelse can get_translation_scheme target)) 140 val target = type_of term value 141 val enc = get_encode_function target t 153 (is_vartype target orels 209 val target = type_of (lhs final) value 274 val target = type_of term value 570 val target = type_of var value 594 val target = type_of encoded_term value 850 val target = (type_of o lhs) final value 1075 val target = type_of (rhs final) value 1264 let val target = type_of (lhs (concl thm)) value 2631 val target = type_of term value 2704 val target = type_of right value 3357 val target = type_of term value 3478 let val target = last (fst (strip_fun (type_of term))) value 3513 let val target = type_of term value 3837 val target = hd (pairSyntax.strip_prod (hd txs)); value 4126 val target = type_of term value [all...] |
H A D | polytypicLib.sml | 168 {target : hol_type, induction : thm, recursion : thm, left : term, right : term, predicate : term, bottom : term, bottom_thm : thm}; 993 (* 'target' function deals with decoding and detecting whereas the *) 1173 "\nis not a valid source or target function", 1180 "\nis not a fully expanded source or target function,\n" ^ 1538 val target = #target scheme value 1540 val x = mk_var("x",target) 1542 raise (mkDebug ("Predicate for translation scheme " ^ type_to_string target ^ 1544 fun mkP y p = mk_comb(mk_var("P" ^ (int_to_string p),target --> ``:bool``),beta_conv (mk_comb(y,x))) 1545 fun mkP_var n = mk_comb(mk_var("P" ^ (int_to_string n),target [all...] |
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | gic_v2.c | 39 /* Get the target id for this processor. We rely on the constraint that the registers 40 * for PPI are read only and return only the current processor as the target. 46 uint32_t target = 0; local 48 target = gic_dist->targets[i >> 2]; 49 target |= target >> 16; 50 target |= target >> 8; 51 if (target) { 55 if (!target) { 88 uint8_t target = infer_cpu_gic_id(nirqs); local 207 setIRQTarget(irq_t irq, seL4_Word target) argument [all...] |
/seL4-l4v-master/isabelle/src/Pure/GUI/ |
H A D | wrap_panel.scala | 26 override def preferredLayoutSize(target: Container): Dimension = 27 layout_size(target, true) 29 override def minimumLayoutSize(target: Container): Dimension = 31 val minimum = layout_size(target, false) 36 private def layout_size(target: Container, preferred: Boolean): Dimension = 38 target.getTreeLock.synchronized 41 if (target.getSize.width == 0) Integer.MAX_VALUE 42 else target.getSize.width 46 val insets = target.getInsets 64 i <- (0 until target [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/GUI/ |
H A D | wrap_panel.scala | 26 override def preferredLayoutSize(target: Container): Dimension = 27 layout_size(target, true) 29 override def minimumLayoutSize(target: Container): Dimension = 31 val minimum = layout_size(target, false) 36 private def layout_size(target: Container, preferred: Boolean): Dimension = 38 target.getTreeLock.synchronized 41 if (target.getSize.width == 0) Integer.MAX_VALUE 42 else target.getSize.width 46 val insets = target.getInsets 64 i <- (0 until target [all...] |
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | cygwin.scala | 46 case target :: content :: rest => 47 link(content, new JFile(isabelle_root, target)) 59 def link(content: String, target: JFile) 61 val target_path = target.toPath
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | cygwin.scala | 46 case target :: content :: rest => 47 link(content, new JFile(isabelle_root, target)) 59 def link(content: String, target: JFile) 61 val target_path = target.toPath
|
/seL4-l4v-master/graph-refine/ |
H A D | target_objects.py | 7 # these objects are to be filled in by the target 79 def load_target (target, target_args = None): 80 target_dir.set_dir (target) 86 pck.__path__.append (target) 88 sys.path.append (target) 89 import target namespace 99 print 'Usage: python %s <target> <instructions>' % objname 102 print 'See example target (in %s)' % exname 104 print 'See example target in graph-refine dir.' 107 target [all...] |
/seL4-l4v-master/seL4/src/kernel/ |
H A D | thread.c | 69 void suspend(tcb_t *target) argument 71 cancelIPC(target); 72 if (thread_state_get_tsType(target->tcbState) == ThreadState_Running) { 78 updateRestartPC(target); 80 setThreadState(target, ThreadState_Inactive); 81 tcbSchedDequeue(target); 83 tcbReleaseRemove(target); 84 schedContext_cancelYieldTo(target); 88 void restart(tcb_t *target) argument 90 if (isStopped(target)) { 522 possibleSwitchTo(tcb_t *target) argument [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sig | 12 (* mc_compile fname target: compiles function fname to target code,
|
H A D | compilerLib.sml | 77 fun basic_compile target tm = let 78 val (tools,target,model_name,s) = 79 if mem target ["arm","ARM"] then (arm_tools,"arm","ARM_MODEL",[]) else 80 if mem target ["x86","i32","386"] then (x86_tools,"x86","X86_MODEL",to_x86_regs ()) else 81 if mem target ["x64","X64"] then (x64_tools,"x64","X64_MODEL",[]) else 82 if mem target ["ppc","Power","PowerPC"] then (ppc_tools,"ppc","PPC_MODEL",[]) else fail() 85 val _ = echo 1 ("\nCompiling " ^ name ^ " into "^ target ^ "...\n") 86 val (code,len) = generate_code target model_name true tm 115 fun compile target tm = let 119 val (th,def,pre) = basic_compile target t [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_DepGraph.sml | 38 type 'a nodeInfo = { target : dep, status : target_status, extra : 'a, 45 val {target,command,status,dependencies,seqnum,phony,dir,extra} = nI value 47 {target = target, status = f status, command = command, seqnum = seqnum, 53 fun addDeps0 dps {target,command,status,dependencies,seqnum,phony,dir,extra} = 54 {target = target, status = status, command = command, phony = phony, 123 target_map = Map.insert(#target_map g, #target nI, n), 127 val {target=tgt,dir,...} = nI 168 val {target,statu value [all...] |
H A D | unix-systeml.sml | 124 fun emit_hol_script target qend _ = let 125 val ostrm = TextIO.openOut target 137 mk_xable target 141 fun emit_hol_unquote_script target qend _ = let 142 val ostrm = TextIO.openOut target 158 mk_xable target
|
/seL4-l4v-master/seL4/src/arch/arm/object/ |
H A D | interrupt.c | 86 seL4_Word target = getSyscallArg(4, buffer); local 89 irq_t irq = CORE_IRQ_TO_IRQT(target, irq_w); 95 if (target >= CONFIG_MAX_NUM_NODES) { 97 userError("Target core %lu is invalid.", target); 126 * target core to which the shared interrupt will be physically delivered. 129 setIRQTarget(irq, target);
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_polyml.scala | 109 ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ 110 rm -rf target 119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines 139 /* target */ 141 val target = Path.explode(platform) 142 Isabelle_System.rm_tree(target) 143 Isabelle_System.mkdirs(target) 146 File.copy(Path.explode(file).expand_env(settings), target) 149 d <- List("target/bin", "target/li [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_polyml.scala | 109 ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ 110 rm -rf target 119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines 139 /* target */ 141 val target = Path.explode(platform) 142 Isabelle_System.rm_tree(target) 143 Isabelle_System.mkdirs(target) 146 File.copy(Path.explode(file).expand_env(settings), target) 149 d <- List("target/bin", "target/li [all...] |
/seL4-l4v-master/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 78 fun emit_hol_script target qend = 79 let val ostrm = fopen(target^".bat") 91 target 95 fun emit_hol_unquote_script target qend = 96 let val ostrm = fopen(target^".bat") 112 target
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | spec_databaseLib.sml | 73 fun current_opt_rule target = convert_opt_rule (basic_opt ()) target 87 fun closest target = fst o utilsLib.maximal Int.compare (closeness target) 88 fun find_closest target = 89 (closest target ## I) o fst o 90 utilsLib.maximal Int.compare (closeness target o closest target o fst)
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | xml.scala | 44 def apply(prefix: String, target: String): Namespace = 45 new Namespace(prefix, target) 48 final class Namespace private(prefix: String, target: String) 51 val attribute: XML.Attribute = ("xmlns:" + prefix, target)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | xml.scala | 44 def apply(prefix: String, target: String): Namespace = 45 new Namespace(prefix, target) 48 final class Namespace private(prefix: String, target: String) 51 val attribute: XML.Attribute = ("xmlns:" + prefix, target)
|
/seL4-l4v-master/seL4/src/arch/riscv/machine/ |
H A D | hardware.c | 238 uint64_t target; local 242 target = riscv_read_time() + RESET_CYCLES; 243 sbi_set_timer(target); 244 } while (riscv_read_time() > target);
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psBigSteps.sml | 158 fun run_bigsteps bsobj target = 164 player = #preplayer bsobj target 166 val (tree,cache) = starttree_of mctsobj target 203 preplayer = fn target => uniform_player toy_game, 208 val target = (0,10,100); 209 val (_,t) = add_time (run_bigsteps bsobj) target; 210 val (winb,rlex,rootl) = run_bigsteps bsobj target;
|
/seL4-l4v-master/graph-refine/seL4-example/ |
H A D | Makefile | 30 TARGET_DIR := target/${TARGET_NAME} 72 TARGET_FILES := target.py CFunctions.txt ASMFunctions.txt 78 TARGET_TGZ := ${TARGET_DIR}/target.tar.gz 104 # FIXME: This should be a prerequisite of some other essential target, 127 ${TARGET_DIR}/target.py: target.py 129 cp target.py $@ 136 ${TARGET_DIR}/target.py \
|