Searched refs:targets (Results 1 - 25 of 28) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sig6 (* supported targets are "arm", "ppc" and "x86" *)
16 (* mc_compile_all fname: compiles function fname to all targets *)
H A DcompilerLib.sml135 val targets = ["ppc","x86","arm"] value
142 val xs = compile_each tm targets
/seL4-l4v-master/seL4/src/arch/arm/machine/
H A Dgic_v2.c48 target = gic_dist->targets[i >> 2];
90 gic_dist->targets[i >> 2] = TARGET_CPU_ALLINT(target);
186 * 23-16: CPU targets list
210 uint8_t *targets = (void *)(gic_dist->targets); local
218 targets[hwIRQ] = targetList;
/seL4-l4v-master/l4v/misc/
H A Disa-common.mk8 # Common build targets for Isabelle Makefiles.
66 # Some targets within this Makefile depend on files, which are managed
76 # Common targets that should be considered PHONY.
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHolmake_types.sig9 type raw_rule_info = { targets : quotation, dependencies : quotation,
45 a list of the targets of the rule.
H A DHolmake.sml78 val (master_cline_options, targets) = getcline (CommandLine.arguments())
503 diag "startup" (fn _ => "Targets = [" ^ String.concatWith ", " targets ^ "]");
902 map, ensuring that if targets are marked as needed, the
1038 case targets of
1041 val targets = if cline_recursive_build then value
1046 mk_dirneeded (hmdir.curdir()) (mkneeded targets depgraph)
1048 mkneeded targets depgraph
1056 "Generated targets are: [" ^concatWithf pr ", " targets ^ "]"
1104 val targets value
[all...]
H A DHolmake_types.sml12 type raw_rule_info = { targets : quotation, dependencies : quotation,
205 targets = extract_normal_quotation tgts}
315 fun extend_ruledb warn env {targets,dependencies,commands} (rdb,ddb) = let
316 val tgts = map dequote (tokenize (perform_substitution env targets))
H A DHM_Core_Cline.sml202 { help = "try to build all targets", long = ["keep-going"], short = "k",
241 { help = "build all targets recursively", short = "",
H A DHolmake_tools.sig141 (* nicely format a list of makefile targets *)
H A DregexpMatch.sml288 val targets = List.map #2 outarcs value
292 work (targets@t) (Q',deltaMap')
H A DHolmake_tools.sml617 (* targets are also dependencies, so the naming convention is to use variable
/seL4-l4v-master/l4v/spec/haskell/include/
H A Dgic.h27 uint32_t targets[255]; /* [0x800, 0xBFC) */ member in struct:gic_dist_map_t
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A DtripleLib.sml53 val targets = progSyntax.strip_star (utilsLib.lhsc assert_rwt) value
91 | NONE => (sbst, t :: frm)) ([], []) targets
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dbuild_fonts.scala230 val targets =
285 (for ((name, index) <- targets if index == 0)
315 (for ((target, _) <- targets) yield
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dbuild_fonts.scala230 val targets =
285 (for ((name, index) <- targets if index == 0)
315 (for ((target, _) <- targets) yield
/seL4-l4v-master/l4v/spec/cspec/c/
H A Dkernel.mk80 # Various targets useful for binary verification.
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/
H A Dgic_v2.h66 uint32_t targets[255]; /* [0x800, 0xBFC) */ member in struct:gic_dist_map
/seL4-l4v-master/HOL4/Manual/Description/
H A Dmisc.tex280 Using a \texttt{Holmakefile} (see Section~\ref{sec:using-Holmakefiles}), it is possible to mention files in other directories, both as dependencies and as explicit targets with rules on how those targets should be built.
287 With \texttt{INCLUDES} information to hand, \holmake{} will process the entire \texttt{INCLUDES} graph, looking throughout the graph for theory files that the current directory may depend on, and rebuilding those remote targets as necessary.
291 Like {\tt make}, \holmake{} takes command-line arguments corresponding to the targets that the user desires to build.
292 As a special case of this, targets ending with the suffix \ml{Theory} are treated as an instruction to build the theory files that lie behind a \HOL{} theory.
294 If there are no command-line targets, then \holmake{} will look for a \texttt{Holmakefile} in the current directory.
295 If there is none, or if that file specifies no targets, then \holmake{} will attempt to build all \ML{} modules and \HOL{} theories it can detect in the current directory.
298 In addition, there are three special targets that can be used:
333 As above, directories specified in this way will also be rebuilt before the current targets are built.
339 to build all specified targets, rathe
[all...]
/seL4-l4v-master/HOL4/src/AI/machine_learning/
H A DmlReinforce.sml289 log rlobj ("Exploration: " ^ its nfin ^ " targets ");
290 log rlobj ("Exploration: " ^ its nwin ^ " targets proven at least once");
/seL4-l4v-master/HOL4/src/quotient/examples/lambda/
H A DtermScript.sml396 (* This involves also the source or bound variables to be the targets *)
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/
H A DhelperLib.sml344 fun LIST_MOVE_OUT_CONV rvs targets =
348 val (ts, l) = List.foldl plkf ([], xs) targets
361 fun MATCH_MOVE_OUT_CONV targets =
365 val (ts, l) = List.foldl plkm ([], xs) targets
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dderive_specsLib.sml317 val targets = zip (genlist I case_count 0) (take case_count (drop 3 raw_code)) value
340 val xs = map eval_case targets
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/
H A DobjectScript.sml435 (* This involves also the source or bound variables to be the targets *)
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dmisc.tex262 to the targets that the user desires to build. If there are none,
265 special targets that can be used:
285 this way will also be rebuilt before the current targets are built.
315 to build all specified targets, rather than stopping as soon as one
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/
H A Dfor_compileScript.sml8 defined in forScript.sml. The compiler targets a simple assembly-like

Completed in 168 milliseconds

12