Searched refs:target (Results 1 - 25 of 140) sorted by relevance

123456

/seL4-l4v-master/seL4/src/object/
H A Dschedcontrol.c13 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 DencodeLib.sml60 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 DfunctionEncodeLib.sml116 (* 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 DpolytypicLib.sml168 {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 Dgic_v2.c39 /* 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 Dwrap_panel.scala26 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 Dwrap_panel.scala26 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 Dcygwin.scala46 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 Dcygwin.scala46 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 Dtarget_objects.py7 # 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 Dthread.c69 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 DcompilerLib.sig12 (* mc_compile fname target: compiles function fname to target code,
H A DcompilerLib.sml77 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 DHM_DepGraph.sml38 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 Dunix-systeml.sml124 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 Dinterrupt.c86 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 Dbuild_polyml.scala109 ./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 Dbuild_polyml.scala109 ./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 DwinNT-systeml.sml78 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 Dspec_databaseLib.sml73 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 Dxml.scala44 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 Dxml.scala44 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 Dhardware.c238 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 DpsBigSteps.sml158 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 DMakefile30 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 \

Completed in 147 milliseconds

123456