/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | Makefile | 3 top: pkg-check.txt 11 pkg-check.txt: PKGS.lsp PKGS.sml 20 @echo "(note-chk-known-package-alist-success \"pkg-check.txt\" state)" >> $(TMPFILE) 22 @$(ACL2) < $(TMPFILE) > pkg-check.out 2> pkg-check.err 23 @if [ ! -e pkg-check.txt ]; then \ 24 echo "FAILURE for pkg-check.txt" ; \ 38 rm -f pkg-check.*
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | check_keywords.scala | 14 check: Set[String], 21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source))) 37 check: Set[String], 45 conflicts(keywords, check, arg._1, arg._2)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | check_keywords.scala | 14 check: Set[String], 21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source))) 37 check: Set[String], 45 conflicts(keywords, check, arg._1, arg._2)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Int32.sml | 34 fun check i = function 43 val fromLarge = check o fromLarge 44 val fromInt = check o fromInt 46 val ~ = check o ~ 47 val op * = check o op * 48 val op + = check o op + 49 val op - = check o op - 50 val op div = check o op div 51 val op mod = check o op mod 52 val quot = check [all...] |
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | linux.scala | 20 /* check system */ 28 if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)") 42 val lines = Isabelle_System.bash("lsb_release -a").check.out_lines 68 echo = true).check 71 progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check 88 val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check 111 " " + Bash.string(name)).check 121 """).check 129 Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check 161 Isabelle_System.bash("pwgen " + length + " 1").check [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | linux.scala | 20 /* check system */ 28 if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)") 42 val lines = Isabelle_System.bash("lsb_release -a").check.out_lines 68 echo = true).check 71 progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check 88 val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check 111 " " + Bash.string(name)).check 121 """).check 129 Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check 161 Isabelle_System.bash("pwgen " + length + " 1").check [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | base_tokens.sml | 23 fun check p exnstring (s,loc) = let function 25 fun check ss = function 28 | SOME (c,ss) => if p c then check ss 31 check (full s) 34 val check_binary = check (fn c => c = #"0" orelse c = #"1") 36 val check_octal = check (fn c => #"0" <= c andalso c <= #"7") 38 val check_hex = check (fn c => (#"0" <= c andalso c <= #"9") orelse 44 val check_decimal = check Char.isDigit "Illegal numeral"
|
H A D | PrecAnalysis.sml | 62 fun check_for_listreductions check rels = 72 check(l,s) = NONE 83 (case check(s, tk1) of 85 (case check(valOf left_opt, tk1) of 93 | SOME l => (case check(l,tk1) of 105 case check (valOf left_opt, tk1) of 107 (case check (s, tk1) of 122 (case check (l, tk1) of 135 case check (valOf left_opt, tk2) of 137 (case check(tk [all...] |
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | mercurial.scala | 41 hg.command("root").check 60 hg.command(cmd, args, repository = false).check 101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check 104 hg.command("heads", opt_template(template), options).check.out_lines 107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" 112 hg.command("paths", args = args, options = options).check.out_lines 115 hg.command("manifest", opt_rev(rev), options).check.out_lines 118 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out 129 hg.command("pull", opt_rev(rev) + optional(remote), options).check 132 rev: String = "", clean: Boolean = false, check [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | mercurial.scala | 41 hg.command("root").check 60 hg.command(cmd, args, repository = false).check 101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check 104 hg.command("heads", opt_template(template), options).check.out_lines 107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" 112 hg.command("paths", args = args, options = options).check.out_lines 115 hg.command("manifest", opt_rev(rev), options).check.out_lines 118 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out 129 hg.command("pull", opt_rev(rev) + optional(remote), options).check 132 rev: String = "", clean: Boolean = false, check [all...] |
/seL4-l4v-master/isabelle/src/Pure/Concurrent/ |
H A D | synchronized.scala | 33 def check(x: A): Option[B] = 44 check(x) match { 51 check(state)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/ |
H A D | synchronized.scala | 33 def check(x: A): Option[B] = 44 check(x) match { 51 check(state)
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | selftest.sml | 30 fun infloop_protect msg check f x = 31 (tprint msg; require (check_result check) f x) 68 "Bounded rewrites branch, and bypass permutative loop check" 88 fun check (th1, th2) = function 93 "Bounded rewrites override mk_rewrites loop check" 94 check 105 fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z`` function 109 check 120 fun check th = not (aconv (rhs (concl th)) ``x:bool``) function 124 check 135 fun check th = aconv (rhs (concl th)) result function 146 fun check th = aconv (rhs (concl th)) result function 157 fun check th = aconv (rhs (concl th)) result function 171 fun check (sgs, vfn) = let function 190 fun check th = th |> concl |> rhs |> aconv F function 200 fun check th = th |> concl |> rhs |> aconv F function [all...] |
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | github115bScript.sml | 5 (* this theory is in the test-case solely to force Holmake to check that the
|
/seL4-l4v-master/HOL4/src/datatype/theory_tests/ |
H A D | ndatatype_ind0Script.sml | 32 fun check (tac, t) = (tac([], t) before ignore (save_thm( function 37 val _ = map check [
|
/seL4-l4v-master/HOL4/src/string/theorytesting/ |
H A D | injected_strlit3Script.sml | 8 (* check that the string injections from the base theory really have been
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_cygwin.scala | 39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check 57 Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
|
H A D | build_polyml.scala | 113 """, redirect = true, echo = true).check 119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines 131 bash(dir1, "./build " + platform_64, redirect = true, echo = true).check 158 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check 164 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check 200 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check 203 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
|
H A D | other_isabelle.scala | 53 other_isabelle("components -a", redirect = true, echo = echo).check 56 other_isabelle("getenv -b " + Bash.string(name)).check.out
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_cygwin.scala | 39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check 57 Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
|
H A D | build_polyml.scala | 113 """, redirect = true, echo = true).check 119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines 131 bash(dir1, "./build " + platform_64, redirect = true, echo = true).check 158 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check 164 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check 200 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check 203 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
|
H A D | other_isabelle.scala | 53 other_isabelle("components -a", redirect = true, echo = echo).check 56 other_isabelle("getenv -b " + Bash.string(name)).check.out
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 205 bool check = false; local 226 check = true; 243 if (proof != NULL || check) S.proof = new Proof(); 252 if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof); 284 if (compress) { // ...compress, and possibly check 288 if (check) 293 } else if (check) { // ...check
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | HolQbfLib.sml | 45 QbfCertificate.VALID _ => QbfCertificate.check t dict cert 60 QbfCertificate.check t dict cert 74 QbfCertificate.check t dict cert 91 val th = QbfCertificate.check t' dict cert
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | SHA1_ML.sig | 8 * always return an empty vector and cannot be used to check for the end
|