| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
| H A D | translationsLib.sml | 341 val args = strip_pair (hd args); value
356 val args = strip_pair (hd args); value
371 val args = strip_pair (hd args); value
386 val args = strip_pair (hd args); value
405 val args = strip_pair (hd args); value
424 val args = strip_pair (hd args); value
443 val args = strip_pair (hd args); value
524 val args = strip_pair (aPair); value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | interpret.cpp | 136 virtual Handle EnterCallbackFunction(Handle func, Handle args) { ASSERT(0); return 0; } argument
[all...] |
| H A D | savestate.cpp | 711 Handle SaveState(TaskData *taskData, Handle args) argument
[all...] |
| H A D | unix_specific.cpp | 395 Handle OS_spec_dispatch_c(TaskData *taskData, Handle args, Handle code) argument
1285 waitForProcess(TaskData *taskData, Handle args) argument
1463 getTTYattrs(TaskData *taskData, Handle args) argument
1503 setTTYattrs(TaskData *taskData, Handle args) argument
1539 lockCommand(TaskData *taskData, int cmd, Handle args) argument
2012 getSysConf(TaskData *taskData, Handle args) argument
[all...] |
| H A D | windows_specific.cpp | 305 Handle OS_spec_dispatch_c(TaskData *taskData, Handle args, Handl argument
857 execute(TaskData *taskData, Handle args) argument
969 simpleExecute(TaskData *taskData, Handle args) argument
1034 openProcessHandle(TaskData *taskData, Handle args, BOOL fIsRead, BOOL fIsText) argument
1085 openRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument
1111 createRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument
1148 deleteRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument
1164 deleteRegistryValue(TaskData *taskData, Handle args, HKEY hkParent) argument
1180 queryRegistryKey(TaskData *taskData, Handle args, HKEY hkey) argument
1240 setRegistryKey(TaskData *taskData, Handle args, HKEY hkey) argument
1272 enumerateRegistry(TaskData *taskData, Handle args, HKEY hkey, BOOL isKey) argument
[all...] |
| H A D | network.cpp | 394 static Handle Net_dispatch_c(TaskData *taskData, Handle args, Handle code) argument
1314 setSocketOption(TaskData *taskData, Handle args, int level, int opt) argument
1326 getSocketOption(TaskData *taskData, Handle args, int level, int opt) argument
1339 getSocketInt(TaskData *taskData, Handle args, int level, int opt) argument
1352 getSelectResult(TaskData *taskData, Handle args, int offset, fd_set *pFds) argument
1381 selectCall(TaskData *taskData, Handle args, int blockType) argument
[all...] |
| H A D | processes.cpp | 770 Handle Processes::ThreadDispatch(TaskData *taskData, Handle args, Handle code) argument
1252 CreateNewTaskData(Handle threadId, Handle threadFunction, Handle args, PolyWord flags) argument
1596 ForkThread(TaskData *taskData, Handle threadFunction, Handle args, PolyWord flags, PolyWord stacksize) argument
[all...] |
| H A D | x86_dep.cpp | 956 Handle X86TaskData::EnterCallbackFunction(Handle func, Handle args) argument
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Prim_rec.sml | 951 val args = snd(strip_comb rhs) value
[all...] |
| H A D | Pmatch.sml | 200 let val (args,plist') = gtake I (L, plist) value
209 let val (args,plist') = gtake I (L, plist) value
274 val args = map mk_arg literals value
591 let val (args,ta value
[all...] |
| H A D | TypeBasePure.sml | 757 (let val args = snd(dest_type ty) value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/ |
| H A D | compile.sml | 127 let val (args,t) = value
1482 val (args,bdy) = dest_pabs abstr value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 524 val args = pairLib.strip_pair arg; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 370 val (args, rst) = split tys r value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | MutRecDef.sml | 423 val {args, ty} = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesSyntax.sml | 859 val args = Lib.mapi (fn i => fn ty => mk_var("x" ^ Int.toString i, ty)) argtys value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 382 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring value
446 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring value
714 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring value
892 val args = ps |> listSyntax.dest_list |> fst |> map stringSyntax.fromHOLstring value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_OPTIMISER.sml | 791 val args = makeArgs(n, hd) value
978 val args = map (fn (c, t) => (optGeneral context c, t)) argList value
1003 val args = map (fn (c, t) => (optGeneral context c, t)) argList value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | TYPEIDCODE.sml | 747 val args = List.tabulate(nTypeVars, fn addr => fn l => mkLoadParam(addr+2, l, baseEqLevelP1)) value
895 val args = List.map(fn addr => fn l => mkLoadParam(addr, l, oldLevel)) argAddrs value
1113 val args = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | CommonDialog.sml | 628 val args = (Word.toInt sizeOfnStruct, (* lStructSize *) value
790 val args = value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | ind_types.sml | 196 val args = make_args "a" [] ttys value
233 val (args,bod) = strip_abs right value
385 val args = make_args "x" [] (map (K recty) preds) value
510 val args = make_args "a" [] domtys value
603 val (args,bod) = strip_abs(rand(hd(hyp cth))) value
707 (fn th => let val args = fst(strip_abs(rand(concl th))) in value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/emit/ |
| H A D | EmitML.sml | 235 val args = vars_of_types argtys value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | term_pp.sml | 1651 val (args,Rand) = front_last args0 value
1827 val (args, Rand) = front_last oiargs value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | sexp.sml | 1076 val args = (flatten o map strip_pair) arg_tuples value
1441 then let val args = map mlsexp_to_term (dest_mlsexp_list y) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | sexp.sml | 1002 val args = (flatten o map strip_pair) arg_tuples value
1367 then let val args = map mlsexp_to_term (dest_mlsexp_list y) value
[all...] |