/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Real.sml | 243 val str = "0." ^ String.implode(List.map toChar digits) ^"E" ^ value 247 val result = realConv str handle RunCall.Conversion _ => raise General.Domain 269 val (str, exp, sign) = dtoa(r, 3, ndigs) value 270 val strLen = String.size str 282 else "0." ^ addZeros(~exp) ^ str ^ addZeros(ndigs-strLen+exp) 287 str ^ addZeros(exp-strLen) ^ 291 String.substring(str, 0, exp) ^ "." ^ 292 String.substring(str, exp, strLen-exp) ^ 305 val (str, exp, sign) = dtoa(r, 2, ndigs+1) value 306 val strLen = String.size str 329 val (str, exp, sign) = dtoa(r, 2, ndigs) value 384 val (str, exp, sign) = dtoa(r, 0, 0) value [all...] |
H A D | Bool.sml | 38 fun scan (getc: (char, 'a) StringCvt.reader) (str: 'a) : (bool * 'a) option = 41 val strm = StringCvt.skipWS getc str
|
H A D | Byte.sml | 48 val (str, offset, size) = Substring.base s value 49 val slice = Word8VectorSlice.slice(stringToBytes str, offset, SOME size)
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sml | 81 | f (ASSIGN_STACK (i,ASSIGN_X_REG d)) = ["str? " ^ r d ^ ", " ^ s i] 82 | f (ASSIGN_STACK (i,ASSIGN_X_CONST j)) = assign_const_to_reg j temp @ ["str? " ^ r temp ^ ", " ^ s i] 83 | f (ASSIGN_MEMORY (ACCESS_WORD,a,ASSIGN_X_REG d)) = ["str? " ^ r d ^ ", " ^ address a] 84 | f (ASSIGN_MEMORY (ACCESS_WORD,a,ASSIGN_X_CONST i)) = assign_const_to_reg i temp @ ["str? " ^ r temp ^ ", " ^ address a]
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | HOLsexp_parser.sml | 46 | SOME (c,cs') => (csref := cs'; str c))
|
H A D | UTF8.sml | 12 else if i < 128 then str (Char.chr i) 86 if i < 128 then SOME((str c, i), string ss') 90 if cnt = 1 then raise BadUTF8 (str c) 138 if pos < 0 then raise BadUTF8 (str (sub(ss,0))) 156 if Char.ord c < 128 then SOME(str c, Char.ord c) 235 | safecp_to_char (RB b) = str (Char.chr b)
|
/seL4-l4v-master/seL4/manual/tools/ |
H A D | parse_doxygen_xml.py | 65 if isinstance(soup, str): 68 string = str(soup) 70 string = str(soup.string) 154 params[str(n.text)] = {"type": param_type} 155 param_order.append(str(n.text)) 216 name = str(member.find('name').string) 545 parser.add_argument("-i", "--input", dest="input", type=str, 547 parser.add_argument("-o", "--output", dest="output", type=str,
|
/seL4-l4v-master/l4v/ |
H A D | run_tests | 72 parser.add_argument('--l4v-arches', metavar='ARCH,...', type=str,
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex.lex | 28 List.foldl (fn ((str, tok), t) => Binarymap.insert (t, str, tok))
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | base_tokens.sml | 13 (case copt of SOME c => String.str c 47 String.translate (fn #"_" => "" | c => str c) s
|
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | graph_to_graph.py | 83 print 'bench returned: ' + str(bench_ret)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | exporter.h | 77 unsigned long makeEntry(const char *str);
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | DataSize.sml | 29 fun pass str = 30 if mem str names 32 else str 127 fun gamma str = 128 case assoc1 str tyop_map 129 of NONE => type_size_env str
|
/seL4-l4v-master/isabelle/src/Pure/Isar/ |
H A D | outer_syntax.scala | 24 def quote_string(str: String): String = 26 val result = new StringBuilder(str.length + 10) 28 for (s <- Symbol.iterator(str)) {
|
/seL4-l4v-master/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 38 (eval_X c env (Const str) = c.parse str)` 187 (x_str (Var str) = str) /\ (x_str (Const str) = str) `
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Isar/ |
H A D | outer_syntax.scala | 24 def quote_string(str: String): String = 26 val result = new StringBuilder(str.length + 10) 28 for (s <- Symbol.iterator(str)) {
|
/seL4-l4v-master/seL4/src/arch/arm/32/ |
H A D | hyp_traps.S | 99 str lr, [sp, #4] 102 str lr, [sp, #8] 111 str lr, [sp, #(PT_FaultIP - PT_SP)]
|
/seL4-l4v-master/HOL4/src/Boolify/src/ |
H A D | Encode.sml | 50 fun pass str = 51 if mem str names 53 else str 165 fun gamma str = 166 case assoc1 str tyop_map 167 of NONE => type_encode_env str
|
/seL4-l4v-master/l4v/tools/haskell-translator/ |
H A D | lhs_pars.py | 516 bstring = braces.str(string, '(', ')') 527 s = str(bit).strip() 531 bit2 = braces.str(s[1:-1], '(', ')') 534 if str(bits[0]) == 'PPtr': 539 arg = ' '.join([str(bit) for bit in bits[1:]])[1:-1] 541 return ' '.join([arg, 'list', str(type_conv(bits[0]))]) 545 strs = [str(bit) for bit in bits] 586 elif str(string) in type_conv_table: 587 result = type_conv_table[str(string)] 599 type_conv_table[str(strin [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 65 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring value 67 in mk_var(str,ty) |-> tm end) 82 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring value 84 in mk_var(str,ty) |-> tm end) 101 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring value 103 in mk_var(str,ty) |-> tm end) 477 val str = ("Graph spec failed in " ^ sec_name ^ " for pos " ^ value 479 in (write_line str; print (str ^ "\n")) end 502 val str value [all...] |
/seL4-l4v-master/graph-refine/ |
H A D | graph-refine.py | 115 return str (result) 127 word_pairs = [p for p in pairs if s in word_re.findall (str (p))] 130 print 'Possibilities for %r: %s' % (s, [str (p) for p in pairs]) 263 return [v for v in vs if type (v) == str] + [v2 264 for v in vs if type (v) != str for v2 in get_strs (v)]
|
H A D | syntax.py | 304 return hash(str(self)) 353 xs.append (str (self.num)) 356 xs.extend ([str (n) for n in self.nums]) 362 xs.append (str (self.num)) 441 if type (nm) == str: 531 xs.append (str (len (self.vals))) 535 xs.append (str (self.val)) 730 xs.extend ([str (c) for c in self.get_conts ()]) 732 xs.append (str (len (self.upds))) 741 xs.append (str (le [all...] |
/seL4-l4v-master/l4v/tools/autocorres/tools/ |
H A D | release.py | 109 type=str, help='Version number of the release, such as "0.95-beta1".') 111 type=str, help='Tarball to the C parser release.') 113 type=str, help='Tarball to the official Isabelle release') 125 type=str, help='Path to the L4.verified repository base.', default=None) 127 type=str, default='ARM,ARM_HYP,X64,RISCV64',
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sml | 78 let val (str , fst , snd) = value 80 (str , [fst , snd]) => (str , fst , snd) 82 val (str , tp_type, b) = value 84 (str , [tp_type, b]) => (str , tp_type, b) 266 val (c,str) = 268 COMB(c,str) => (c,str) 278 str,uf_fu 364 val str = valOf (TextIO.inputLine TextIO.stdIn) value [all...] |
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Htmlsigs.sml | 75 | Str => "str" 158 | encode c = str c 263 dec "str" 347 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn) 363 (fn c => (href (str c) ("#" ^ str c); out " ")) 376 app out ["\n</ul>\n\n<a name=\"", str c1, "\">"]; 377 subheader (str c1);
|