/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sig | 6 (* supported targets are "arm", "ppc" and "x86" *) 16 (* mc_compile_all fname: compiles function fname to all targets *)
|
H A D | compilerLib.sml | 135 val targets = ["ppc","x86","arm"] value 142 val xs = compile_each tm targets
|
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | gic_v2.c | 48 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 D | isa-common.mk | 8 # 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 D | Holmake_types.sig | 9 type raw_rule_info = { targets : quotation, dependencies : quotation, 45 a list of the targets of the rule.
|
H A D | Holmake.sml | 78 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 D | Holmake_types.sml | 12 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 D | HM_Core_Cline.sml | 202 { help = "try to build all targets", long = ["keep-going"], short = "k", 241 { help = "build all targets recursively", short = "",
|
H A D | Holmake_tools.sig | 141 (* nicely format a list of makefile targets *)
|
H A D | regexpMatch.sml | 288 val targets = List.map #2 outarcs value 292 work (targets@t) (Q',deltaMap')
|
H A D | Holmake_tools.sml | 617 (* targets are also dependencies, so the naming convention is to use variable
|
/seL4-l4v-master/l4v/spec/haskell/include/ |
H A D | gic.h | 27 uint32_t targets[255]; /* [0x800, 0xBFC) */ member in struct:gic_dist_map_t
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | tripleLib.sml | 53 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 D | build_fonts.scala | 230 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 D | build_fonts.scala | 230 val targets = 285 (for ((name, index) <- targets if index == 0) 315 (for ((target, _) <- targets) yield
|
/seL4-l4v-master/l4v/spec/cspec/c/ |
H A D | kernel.mk | 80 # Various targets useful for binary verification.
|
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
H A D | gic_v2.h | 66 uint32_t targets[255]; /* [0x800, 0xBFC) */ member in struct:gic_dist_map
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | misc.tex | 280 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 D | mlReinforce.sml | 289 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 D | termScript.sml | 396 (* This involves also the source or bound variables to be the targets *)
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 344 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 D | derive_specsLib.sml | 317 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 D | objectScript.sml | 435 (* This involves also the source or bound variables to be the targets *)
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 262 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 D | for_compileScript.sml | 8 defined in forScript.sml. The compiler targets a simple assembly-like
|