/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_prover_extLib.sml | 112 let val (str , fst , snd) = value 114 (str , [fst , snd]) => (str , fst , snd) 116 val (str , tp_type, b) = value 118 (str , [tp_type, b]) => (str , tp_type, b) 273 (str , [fst , snd]) => 433 (*val (str , [fst , snd]) = dest_type (type_of a_body) *) 434 (* val (str , [a_body_type, b]) = dest_type snd;*) 635 (*val (str , [fs [all...] |
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | pydot.py | 245 The values can be anything: bool, int, float, str. 259 if isinstance(edge[0], str): 262 src = node_prefix + str(edge[0]) 264 if isinstance(edge[1], str): 267 dst = node_prefix + str(edge[1]) 765 name = str(name) 948 if not isinstance(node_str, str): 985 edge = [ str(src) ] 1001 edge.append( str(dst) ) 1271 raise TypeError('add_node() received a non node class object: ' + str(graph_nod [all...] |
H A D | cplex.py | 165 print "the unbounded variable is : %s" % str(var_s)
|
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | sptreeSyntax.sml | 197 val {add_string = str, add_break = brk, ublock, ...} = 204 Prec (j, _) => if 200 <= j then str s else nothing 211 >> str "sptree$fromAList" 219 >> str "sptree$fromList"
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | OldPP.sig | 109 [add_stringsz ppstrm str] outputs the string str to the ppstream 112 [add_string ppstrm (str,sz)] outputs the string str to the ppstream
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | GetOpt.sml | 48 fun fmtShort (NoArg _) so = concat ["-", str so] 49 | fmtShort (ReqArg (_,ad)) so = concat ["-", str so," ",ad] 50 | fmtShort (OptArg (_,ad)) so = concat ["-", str so,"[",ad,"]"] 154 val optStr = "-"^(str x)
|
H A D | Holmake_types.sml | 35 str startc ^ 94 | _ => extract (LIT ("\\" ^ str c) :: acc) rest' 112 extract (VREF (str c) :: acc) rest 114 raise Fail ("Bad variable name: "^str c) 297 if quotable c then recurse (str c :: acc) rest 298 else recurse (str c :: "\\" :: acc) rest
|
H A D | HM_GraphBuildJ1.sml | 33 fun str (n,nI) = node_toString n ^ ": " ^ nodeInfo_toString pr nI function 39 diagK ("Failed nodes: \n" ^ String.concatWith "\n" (map str ns));
|
H A D | unix-systeml.sml | 22 fun unix_trans c = if is_meta c then "\\" ^ str c else str c
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/ |
H A D | BuildCommand.sml | 13 fun variant str = (* get an unused file name in the current directory *) 14 if FileSys.access(str,[]) 16 let val s = str^Int.toString i 21 else str;
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
H A D | arm_evalLib.sig | 42 |> arm_load_from_string "A00" "thumb\n str r1,[r0],#4"
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/standalone-parser/ |
H A D | GetOpt.sml | 51 fun fmtShort (NoArg _) so = concat ["-", str so] 52 | fmtShort (ReqArg (_,ad)) so = concat ["-", str so," ",ad] 53 | fmtShort (OptArg (_,ad)) so = concat ["-", str so,"[",ad,"]"] 157 val optStr = "-"^(str x)
|
/seL4-l4v-10.1.1/l4v/misc/autostop/ |
H A D | stop.c | 71 fatal(const char *str) argument 73 printf("%s\n", str);
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | options.scala | 357 def + (str: String): Options = 359 str.indexOf('=') match { 360 case -1 => this + (str, None) 361 case i => this + (str.substring(0, i), str.substring(i + 1))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | options.scala | 357 def + (str: String): Options = 359 str.indexOf('=') match { 360 case -1 => this + (str, None) 361 case i => this + (str.substring(0, i), str.substring(i + 1))
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | loop_bounds.py | 75 #print 'restrs: %s' % str(restrs) 324 assert str (kind) == kind 325 return [hex (addr), str (bound), kind] 336 ss += [str (len (call_ctxt))] + map (hex, call_ctxt) 337 ss += [str (prob_hash)] 341 ss += [str (len (prev_bounds))] 350 ctxt2 = ' '.join ([str (len (ctxt2))] + map (hex, ctxt2)) 357 ss = ['ExtraTiming', nm, str (len (ctxt))] + map (hex, ctxt) + [str(time)] 719 trace ('using unique calling context %s' % str ((spli [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | coreScript.sml | 94 ((is = t3) /\ ((ic = ldr) \/ (ic = str) \/ (ic = swp)) \/ 99 ((ic = ldr) \/ (ic = str) \/ (ic = swp)) /\ (is = t3) \/ 109 (is = t3) /\ ((ic = str) \/ (ic = mcr) /\ ~cpb) \/ 128 else if (is = t4) /\ ((ic = ldr) \/ (ic = str)) then 154 (ic = ldr) \/ (ic = str) \/ (ic = ldm) \/ (ic = stm) \/ 241 else if (ic = ldr) \/ (ic = str) then 262 (ic = ldr) \/ (ic = str)) \/ 269 else if (is = t3) /\ (ic = mla_mul) \/ (is = t4) /\ (ic = str) \/ 282 if (ic = data_proc) \/ (ic = ldr) \/ (ic = str) \/ 311 (~bit25 /\ ((ic = ldr) \/ (ic = str))) \/ [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | make_sexp.ml | 74 val _ = declare_names ("ACL2_STRING", "str"); 133 `(stringp(str x) = t) /\ (stringp _ = nil)`; 687 `(coerce (str s) y = 690 else str "") 695 else str(coerce_list_to_string(make_character_list(cons a x)))) 697 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`; 878 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str "")) 880 (symbol_name _ = (str ""))`; 894 ite (symbolp (sym p n)) (str [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexpScript.sml | 96 val _ = declare_names ("ACL2_STRING", "str"); 159 `(stringp(str x) = t) /\ (stringp _ = nil)`; 680 (sexp_size (str a) = 1) /\ 728 `(coerce (str s) y = 731 else str "") 736 else str(coerce_list_to_string(make_character_list(cons a x)))) 738 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`; 1152 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str "")) 1154 (symbol_name _ = (str ""))`; [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexpScript.sml | 96 val _ = declare_names ("ACL2_STRING", "str"); 159 `(stringp(str x) = t) /\ (stringp _ = nil)`; 680 (sexp_size (str a) = 1) /\ 728 `(coerce (str s) y = 731 else str "") 736 else str(coerce_list_to_string(make_character_list(cons a x)))) 738 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`; 1152 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str "")) 1154 (symbol_name _ = (str ""))`; [all...] |
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_initScript.sml | 33 !str. (FST p = read_sexps str) ==> R_exec (str,SND p) q``, 37 \\ Cases_on `is_eof str` 288 val str = tm |> rator |> rator |> rator |> rator |> rator |> rand value 291 val _ = print str
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Overload.sml | 518 fun remove_omapping t str opdict = let 519 val (dictlessk, kitem) = Binarymap.remove(opdict, str) 524 else Binarymap.insert(dictlessk, str, new_rec) 527 fun gen_remove_mapping str t ((opc, cop) : overload_info) = let 530 val ds' = PMDataSet.filter (fn (_, s, _) => s <> str) ds 542 (remove_omapping t str opc, cop') 544 fun remove_mapping str crec = gen_remove_mapping str (prim_mk_const crec)
|
H A D | testutils.sml | 109 fun pretty s = s |> String.translate (fn #"\n" => "\\n" | c => str c) 120 fun f s = String.translate (fn #" " => UTF8.chr 0x2423 | c => str c) s
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | make_iss.sml | 15 String.translate (fn #" " => "-" | c => str (Char.toLower c)) sysname 115 fun trans #"/" = "\\" | trans x = str x
|
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | unix-systeml.sml | 22 fun unix_trans c = if is_meta c then "\\" ^ str c else str c
|