/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | MB_Monitor.sml | 71 fun statusString (MRunning c) = StringCvt.padLeft #" " 3 (str c)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_tools.sml | 826 let val str = Binaryset.foldl (fn (e, A) => p e ^ d :: A) [] set value 829 case str of 831 | _ => String.extract(str, 0, SOME (size str - size d))
|
/seL4-l4v-master/seL4/tools/ |
H A D | lex.py | 57 StringTypes = (str, bytes) 89 return str(self)
|
/seL4-l4v-master/seL4/libsel4/arch_include/arm/sel4/arch/ |
H A D | syscalls.h | 587 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) argument 589 for (char *s = str; *s; s++) {
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 818 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) argument 820 for (char *s = str; *s; s++) {
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls.h | 591 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) argument 593 for (char *s = str; *s; s++) {
|
/seL4-l4v-master/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 111 String.translate (fn c => if c = #"\t" then boldred "\\t" else str c)
|
/seL4-l4v-master/HOL4/src/proofman/tests/ |
H A D | selftest.sml | 111 val strings = map str (explode s)
|
/seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/ |
H A D | syscalls.h | 789 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) argument 791 for (char *s = str; *s; s++) {
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | TopLevelPolyML.sml | 173 then readToEscape(soFar ^ str #"\u001b", terminator) 174 else protocolError(str ch ^ " not " ^ str terminator) 176 | SOME ch => readToEscape(soFar ^ str ch, terminator) 189 | SOME ch => protocolError(str ch ^ " not ESCAPE at start of packet") 325 fun printEsc ch = print (String.concat["\u001b", String.str ch]) 339 fun printEsc ch = print (String.concat["\u001b", String.str ch])
|
/seL4-l4v-master/graph-refine/ |
H A D | search.py | 463 if type (s) == str: 585 if type (p) != str] 1151 trace ('Testing guess for pair: %s' % str (pair)) 1217 if str (it[1][1]) == 'InductFailed'] 1691 return str (n) 1720 printout ("Decided to case split at %s" % str (details)) 1725 printout ('Found a future induction at %s' % str (details[0]))
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 205 iss.str(line);
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | extendTranslateScript.sml | 1393 val STRING_STRCAT = prove(``str (STRCAT s1 s2) = acl2_strcat (str s1) (str s2)``, 1408 val STRING_PREFIX = prove(``bool (isPREFIX s1 s2) = ite (not (less (length (str s2)) (length (str s1)))) 1409 (equal (coerce (str s1) (sym "COMMON-LISP" "LIST")) (acl2_take (length (str s1)) (coerce (str s2) (sym "COMMON-LISP" "LIST")))) nil``,
|
H A D | acl2encodeLib.sml | 218 {const = ``str``,definition = combinTheory.I_THM, induction = NONE}; 242 (simple_encode_map_encode ``str``) 254 ("str ?", op&&& o (equal ``str`` ## stringSyntax.is_string_literal) o dest_comb);
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sml | 188 "\\" ^ String.str ch 191 String.str ch
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | run_tests.py | 339 return ("Exception launching timeout_output: %s" % str(e))
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | SharingTables.sml | 110 SOME str => SOME (TYV str)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_decomp_demoScript.sml | 155 e52d4004 (* push {r4} ; (str *)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | parse_type.sml | 198 "'" ^ str (Char.chr (i - 0x3B1 + Char.ord #"a"))
|
H A D | selftest.sml | 416 val _ = parsetest (map str (explode "ab")) 417 val _ = parsetest (map str (explode "abcdef")) 569 mk_list00 elty n c (map (fn c => mk_var(str c, elty)) (String.explode s))
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape 59 | NONE => str c 117 fun charWord c = mkWord (str c);
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | lisp_gcScript.sml | 54 E4835004 (* L2:str r5,[r3],#4 *) 55 E4836004 (* str r6,[r3],#4 *)`; 69 E4895004 (* str r5,[r9],#4 *) 81 E509501C (* str r5,[r9,#-28] *) 84 E5895004 (* str r5,[r9,#4] *) 105 E5893000 (* str r3,[r9] *)`; 114 E5093018 (* str r3,[r9,#-24] *) 115 E5094014 (* str r4,[r9,#-20] *) 116 E5095010 (* str r5,[r9,#-16] *) 117 E509600C (* str r [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape 59 | NONE => str c 117 fun charWord c = mkWord (str c);
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 297 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 1276 ("(str " ^ "\"" ^ s ^ "\")") 1295 ("(str " ^ "\"" ^ s ^ "\")") 1316 ``str ^(abbrevMLstring s)`` 1338 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1423 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 272 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 1202 ("(str " ^ "\"" ^ s ^ "\")") 1221 ("(str " ^ "\"" ^ s ^ "\")") 1242 ``str ^(abbrevMLstring s)`` 1264 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1349 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
|