/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | reals.cpp | 107 POLYEXTERNALSYMBOL POLYUNSIGNED PolyRealBoxedToString(FirstArgument threadId, PolyWord arg, PolyWord mode, PolyWord digits); 108 POLYEXTERNALSYMBOL POLYUNSIGNED PolyRealGeneral(FirstArgument threadId, PolyWord code, PolyWord arg); 110 POLYEXTERNALSYMBOL POLYUNSIGNED PolyRealBoxedToLongInt(FirstArgument threadId, PolyWord arg); 111 POLYEXTERNALSYMBOL double PolyRealSqrt(double arg); 112 POLYEXTERNALSYMBOL double PolyRealSin(double arg); 113 POLYEXTERNALSYMBOL double PolyRealCos(double arg); 114 POLYEXTERNALSYMBOL double PolyRealArctan(double arg); 115 POLYEXTERNALSYMBOL double PolyRealExp(double arg); 116 POLYEXTERNALSYMBOL double PolyRealLog(double arg); 117 POLYEXTERNALSYMBOL double PolyRealTan(double arg); 249 PolyFloatArbitraryPrecision(PolyWord arg) argument 255 PolyRealBoxedToLongInt(FirstArgument threadId, PolyWord arg) argument 274 PolyRealSqrt(double arg) argument 280 PolyRealSin(double arg) argument 286 PolyRealCos(double arg) argument 292 PolyRealArctan(double arg) argument 298 PolyRealExp(double arg) argument 304 PolyRealLog(double arg) argument 316 PolyRealTan(double arg) argument 321 PolyRealArcSin(double arg) argument 328 PolyRealArcCos(double arg) argument 335 PolyRealLog10(double arg) argument 346 PolyRealSinh(double arg) argument 351 PolyRealCosh(double arg) argument 356 PolyRealTanh(double arg) argument 361 PolyRealFloor(double arg) argument 366 PolyRealCeil(double arg) argument 371 PolyRealTrunc(double arg) argument 378 PolyRealRound(double arg) argument 446 PolyRealFrexp(FirstArgument threadId, PolyWord arg) argument 473 PolyRealFSqrt(float arg) argument 479 PolyRealFSin(float arg) argument 485 PolyRealFCos(float arg) argument 491 PolyRealFArctan(float arg) argument 497 PolyRealFExp(float arg) argument 503 PolyRealFLog(float arg) argument 514 PolyRealFTan(float arg) argument 519 PolyRealFArcSin(float arg) argument 526 PolyRealFArcCos(float arg) argument 533 PolyRealFLog10(float arg) argument 544 PolyRealFSinh(float arg) argument 549 PolyRealFCosh(float arg) argument 554 PolyRealFTanh(float arg) argument 588 PolyRealFFloor(float arg) argument 593 PolyRealFCeil(float arg) argument 598 PolyRealFTrunc(float arg) argument 605 PolyRealFRound(float arg) argument [all...] |
H A D | polyffi.cpp | 94 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFICreateExtFn(FirstArgument threadId, PolyWord arg); 95 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFICreateExtData(FirstArgument threadId, PolyWord arg); 97 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFIMalloc(FirstArgument threadId, PolyWord arg); 98 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFIFree(PolyWord arg); 99 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFILoadLibrary(FirstArgument threadId, PolyWord arg); 101 POLYEXTERNALSYMBOL POLYUNSIGNED PolyFFIUnloadLibrary(FirstArgument threadId, PolyWord arg); 110 POLYUNSIGNED PolyFFIMalloc(FirstArgument threadId, PolyWord arg) argument 119 POLYUNSIGNED size = getPolyUnsigned(taskData, arg); 131 POLYUNSIGNED PolyFFIFree(PolyWord arg) argument 133 void* mem = *(void**)(arg 138 PolyFFILoadLibrary(FirstArgument threadId, PolyWord arg) argument 214 PolyFFIUnloadLibrary(FirstArgument threadId, PolyWord arg) argument 338 PolyFFICreateExtFn(FirstArgument threadId, PolyWord arg) argument 360 PolyFFICreateExtData(FirstArgument threadId, PolyWord arg) argument [all...] |
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 133 "B:" -> (arg => base = arg), 135 "P:" -> (arg => 136 package_collections.get(arg) match { 138 case None => error("Unknown package collection " + quote(arg)) 140 "l:" -> (arg => logic = arg), 142 "o:" -> (arg => output = Some(Path.explode(arg))), 143 "p:" -> (arg [all...] |
H A D | update.scala | 99 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), 100 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), 102 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), 104 "b:" -> (arg => logic = arg), 105 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 133 "B:" -> (arg => base = arg), 135 "P:" -> (arg => 136 package_collections.get(arg) match { 138 case None => error("Unknown package collection " + quote(arg)) 140 "l:" -> (arg => logic = arg), 142 "o:" -> (arg => output = Some(Path.explode(arg))), 143 "p:" -> (arg [all...] |
H A D | update.scala | 99 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), 100 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), 102 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), 104 "b:" -> (arg => logic = arg), 105 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), [all...] |
/seL4-l4v-master/isabelle/src/Pure/ML/ |
H A D | ml_console.scala | 41 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 42 "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), 43 "l:" -> (arg => logic = arg), 44 "m:" -> (arg => modes = arg :: modes), 45 "n" -> (arg => no_build = true), 46 "o:" -> (arg [all...] |
H A D | ml_process.scala | 173 "T:" -> (arg => 174 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), 175 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 176 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), 177 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), 178 "l:" -> (arg => logic = arg), [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/ |
H A D | ml_console.scala | 41 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 42 "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), 43 "l:" -> (arg => logic = arg), 44 "m:" -> (arg => modes = arg :: modes), 45 "n" -> (arg => no_build = true), 46 "o:" -> (arg [all...] |
H A D | ml_process.scala | 173 "T:" -> (arg => 174 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), 175 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 176 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), 177 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), 178 "l:" -> (arg => logic = arg), [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | cpsScript.sml | 40 `CPS f = \k arg. k (f arg)`; 54 ``CPS f k = \arg. let z = f arg in k z``, 64 `(!f g. (f = CPS g) ==> (f = (CPS (\arg. f (\x.x) arg)))) /\ 65 (!f. f arg = (CPS f) (\x.x) arg)`, 76 `CPS2 f = \k1 k2 arg. if f arg the [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | cpsScript.sml | 40 `CPS f = \k arg. k (f arg)`; 54 ``CPS f k = \arg. let z = f arg in k z``, 64 `(!f g. (f = CPS g) ==> (f = (CPS (\arg. f (\x.x) arg)))) /\ 65 (!f. f arg = (CPS f) (\x.x) arg)`, 76 `CPS2 f = \k1 k2 arg. if f arg the [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | cpsScript.sml | 40 `CPS f = \k arg. k (f arg)`; 54 ``CPS f k = \arg. let z = f arg in k z``, 64 `(!f g. (f = CPS g) ==> (f = (CPS (\arg. f (\x.x) arg)))) /\ 65 (!f. f arg = (CPS f) (\x.x) arg)`, 76 `CPS2 f = \k1 k2 arg. if f arg the [all...] |
/seL4-l4v-master/HOL4/tools/ |
H A D | buildcline.sig | 8 update : {warn: string -> unit, die : string -> unit, arg: 'a} -> 'a
|
H A D | buildcline.sml | 7 update : {warn:string -> unit, die:string -> unit, arg:'a} -> 'a 53 NoArg (fn () => { update = fn {warn,die,arg} => updateT arg (U sel b) $$ }) 56 fn {warn,die,arg} => updateT arg (U sel (SOME b)) $$ }) 59 ReqArg ((fn s => { update = fn {warn=wn,die,arg} => 61 NONE => (die ("Couldn't read integer from "^s); arg) 63 (wn ("Ignoring negative number for "^nm); arg) 65 updateT arg (U sel i) $$ }), 68 ReqArg ((fn s => { update = fn {warn=wn,die,arg} [all...] |
/seL4-l4v-master/seL4/src/machine/ |
H A D | io.c | 150 union arg { union 156 static void pop_arg(union arg *arg, int type, va_list *ap) argument 160 arg->p = va_arg(*ap, void *); 163 arg->i = va_arg(*ap, int); 166 arg->i = va_arg(*ap, unsigned int); 169 arg->i = va_arg(*ap, long); 172 arg->i = va_arg(*ap, unsigned long); 175 arg->i = va_arg(*ap, long long); 178 arg 275 union arg arg; local [all...] |
/seL4-l4v-master/graph-refine/ |
H A D | graph-refine.py | 278 for arg in args: 281 if arg == 'verbose': 283 elif arg.startswith ('trace-to:'): 284 (_, s) = arg.split (':', 1) 287 elif arg == 'all': 290 elif arg == 'all_safe': 295 elif arg == 'coverage': 299 elif arg.startswith ('div:'): 300 [_, num, denom] = arg.split (':') 305 elif arg [all...] |
H A D | target_objects.py | 108 t_args = [arg[7:] for arg in args 109 if arg.startswith ('target:')] 110 args = [arg for arg in args[2:] 111 if not arg.startswith ('target:')]
|
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
H A D | MLY_join.sml | 44 type arg = ParserData.arg type 49 val parse = fn (lookahead,lexer,error,arg) => 55 arg=arg, 88 type arg = ParserData.arg type 89 type lexarg = Lex.UserDeclarations.arg 94 val makeLexer = fn s => fn arg => 95 LrParser.Stream.streamify (Lex.makeLexer s arg) [all...] |
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | join.sml | 25 type arg = ParserData.arg type 30 val parse = fn (lookahead,lexer,error,arg) => 36 arg=arg, 69 type arg = ParserData.arg type 70 type lexarg = Lex.UserDeclarations.arg 75 val makeLexer = fn s => fn arg => 76 LrParser.Stream.streamify (Lex.makeLexer s arg) [all...] |
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | join.sml | 25 type arg = ParserData.arg type 30 val parse = fn (lookahead,lexer,error,arg) => 36 arg=arg, 69 type arg = ParserData.arg type 70 type lexarg = Lex.UserDeclarations.arg 75 val makeLexer = fn s => fn arg => 76 LrParser.Stream.streamify (Lex.makeLexer s arg) [all...] |
/seL4-l4v-master/HOL4/examples/hardware/port-full/tamarack2/ |
H A D | tamarackScript.sml | 87 (mem,mar,pc,acc,ir,arg,buf)) = 98 REG ((warg,gnd,bus,bus,arg),P) /\ 99 ALU (n+3) (alu0,alu1,arg,bus,alu) /\ 189 `Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) = 199 (mem,mar,pc,acc,ir,arg,buf))`; 321 ``!n mpc mem mar pc acc ir arg buf. 322 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 334 ``!n mpc mem mar pc acc ir arg buf. 335 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 347 ``!n mpc mem mar pc acc ir arg bu [all...] |
/seL4-l4v-master/HOL4/src/1/ |
H A D | BoundedRewrites.sml | 18 val arg = rand h value 20 (PROVE_HYP (EQ_MP (SYM (SPEC arg BOUNDED_THM)) TRUTH) th, 21 valOf (Int.fromString (#1 (dest_var arg))))
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | proof1.ml | 143 "!n mpc mem mar pc acc ir arg buf. 144 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 157 "!n mpc mem mar pc acc ir arg buf. 158 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 171 "!n mpc mem mar pc acc ir arg buf. 172 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 204 "!n mpc mem mar pc acc ir arg buf. 205 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 219 "!n mpc mem mar pc acc ir arg buf. 220 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,bu [all...] |
/seL4-l4v-master/HOL4/examples/hardware/port/tamarack2/ |
H A D | tamarackProof1Script.sml | 150 ``!n mpc mem mar pc acc ir arg buf. 151 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 165 ``!n mpc mem mar pc acc ir arg buf. 166 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 179 ``!n mpc mem mar pc acc ir arg buf. 180 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 216 ``!n mpc mem mar pc acc ir arg buf. 217 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) 232 ``!n mpc mem mar pc acc ir arg buf. 233 Tamarack n (mpc,mem,mar,pc,acc,ir,arg,bu [all...] |