/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | sharedata.cpp | 76 normally in ML but could be produced as a result of locking mutable objects. 108 because of the possibility of missing an update as a result of breaking a 1056 ShareRequest(Handle root): MainThreadRequest(MTP_SHARING), shareRoot(root), result(false) {} 1068 result = s.RunShareData(shareRoot->WordP()); 1071 bool result; 1089 if (! request.result) 1110 if (! request.result)
|
H A D | x86_dep.cpp | 476 // Called from the assembly code as a result of a trap i.e. a request for 518 // to result in a call here. 832 // Called as a result of a heap overflow trap 902 // result of an RTS call in which case the caller will check this. It can 1227 POLYUNSIGNED result = X86AsmAtomicDecrement(p); local 1228 return this->saveVec.push(PolyWord::FromUnsigned(result));
|
H A D | profiling.cpp | 517 Handle result = 0; local 520 result = profilerc(taskData, pushedMode); 525 if (result == 0) return TAGGED(0).AsUnsigned(); 526 else return result->Word().AsUnsigned();
|
H A D | interpret.cpp | 179 // Put a real result in a "box" 489 case INSTR_deleteHandler: /* Delete handler retaining the result. */ 495 *sp = u; // Put back the result 576 stackItem result = *sp++; /* Result */ local 582 *(--sp) = result; /* Result */ 823 POLYUNSIGNED result = doCall(); local 827 *(--sp) = PolyWord::FromUnsigned(result); 837 POLYUNSIGNED result = doCall(rtsArg1); local 841 *(--sp) = PolyWord::FromUnsigned(result); 852 POLYUNSIGNED result local 868 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3); local 885 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3, rtsArg4); local 903 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3, rtsArg4, rtsArg5); local 916 POLYUNSIGNED result = doCall(this->threadObject); local 930 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1); local 945 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1, rtsArg2); local 961 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1, rtsArg2, rtsArg3); local 1474 int result = memcmp(arg1Ptr+arg1Offset, arg2Ptr+arg2Offset, length); local [all...] |
H A D | pexport.cpp | 447 bool GetValue(PolyWord *result); 474 bool PImport::GetValue(PolyWord *result) argument 483 *result = objMap[obj]; 494 *result = TAGGED(j); 507 PolyWord result = TAGGED(0); local 508 if (GetValue(&result)) 510 p->Set(i, result);
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordsLib.sml | 2712 Guessing the word length for the result of extraction (><),
|
/seL4-l4v-master/seL4/src/arch/x86/64/kernel/ |
H A D | vspace.c | 1613 readWordFromVSpace_ret_t result; local 1614 result = readWordFromVSpace(vspace_root, address); 1615 if (result.status == EXCEPTION_NONE) { 1616 printf("0x%lx: 0x%lx\n", (long)address, (long)result.value);
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODE.sml | 234 | (FunctionType{arg=arg1, result=result1}, FunctionType{arg=arg2, result=result2}) => 810 (* Get the constructor argument given the result type. We might 1270 (* The final result function must take a single argument. *)
|
H A D | SIGNATURES.sml | 521 (* Link together and share two IDs. The result is an equality type if either 639 the result list is all those structures/types with the same name. *) 645 different structures. Then filter the result to produce sets of items 646 with the same name. Discard singletons in the result. *) 799 (* We construct the signature into the result signature. When we apply the 894 is only set to a type that permits equality and that the result 945 IDs (and bound IDs?) as a result of "where type" constraints. *) 1032 val result = pStruct t (offset + 1); value 1038 result (* One slot for each structure. *) 1303 the result o [all...] |
H A D | DEBUGGER_.sml | 131 (SOME result, _) => SOME result
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 130 (* Return the argument/result type which is currently just floating point or everything else. *) 142 create the result tuple on the stack and avoid garbage collector 666 (* TODO: This is a bit of a mess. We want to return the result of the 1002 the constructors but the result shouldn't. For the moment 1135 (* Each function may result in either one or two functions 1213 (* If we're debugging we want the result of the function so we don't do this optimisation. *) 1224 result is general. *) 1317 (* The poly args come after any result tuple. *) 1403 (* If the result is a tuple we try to avoid creating it by adding 1405 the result [all...] |
H A D | MATCH_COMPILER.sml | 661 (* The result of compiling the pattern match code. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 354 (* RTS call with one double-precision floating point argument and a floating point result. *) 358 (* RTS call with two double-precision floating point arguments and a floating point result. *) 363 floating point result. *) 367 (* RTS call with one general (i.e. ML word) argument and a floating point result. 381 floating point result. *) 385 (* RTS call with one general (i.e. ML word) argument and a floating point result. 456 (* Build a foreign call function. The arguments are the abi, the list of argument types and the result type. 457 The result is the code of the ML function that takes three arguments: the C function to call, the arguments 458 as a vector of C values and the address of the memory for the result. *) 468 fun call32Bits(abi, args, result) [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 322 val result = value 370 SOME(mkEnv(List.rev decAddress, result)) 421 mkEnv(combinedDecs @ makeMoves 0, CodeZero (* unit result *)) 523 simpSpecial(envExp, context, decs) (* End of the list - process the result expression. *) 630 heap. It should be optimised away as a result of a further pass but we 755 (* Functions marked as inline could become recursive as a result of 762 can be the result of creating both a general and special function 818 we are trying to expand. This could result in an infinitely recursive expansion. It is only 933 (* NotBoolean: This can be the result of using Bool.not but more usually occurs as a result [all...] |
H A D | CODETREE_OPTIMISER.sml | 297 (* If the result is also curried extend the list. *) 365 (* If the result is just a function where all the arguments are simple 407 (* If the result of a function contains a tuple but it is not detupled on 418 one branch it is probably worth attempting to detuple the result. *) 443 Transform it to take a container as an argument and put the result in there. *) 453 (* The main function performs the previous computation but puts the result into 575 However the usage information is propagated so that if the result of 615 (* We need a container here for the result. *) 813 (* Transforming a lambda may result in producing auxiliary functions that are in 890 (* If the result o [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Foreign.sml | 527 (* This forces the symbol to be loaded. The result is NOT memoised. *) 620 (* The result function. *) 2284 (* Similar to cStar but without the need to update the result. *) 2423 val result = resLoad resultAddr value 2427 result 2447 (* Allocate space for argument and result. *) 2460 val result = resLoad rMem value 2464 result 2705 (* Ignore the result of #store resConv. What this means is if the 2722 val result value 2744 val result = f mlArgs value 2768 val result = f mlArgs value 2795 val result = f mlArgs value 2824 val result = f mlArgs value 2854 val result = f mlArgs value [all...] |
H A D | OS.sml | 963 then raise SysErr("Invalid result", NONE) 968 (* The poll descriptor and the result of polling is a 1081 (* The result is in the corresponding index position. We need to AND this 1084 val result = Word.andb(bits, Vector.sub(resV, index)) value 1086 if result = 0w0 1088 else PI(result, request) :: tl 1112 (* Run a process and wait for the result. *) 1118 val exitResult = LibrarySupport.volatileOptionRef() (* Set to the exit result. *) 1127 (* Exit. Run the atExit functions and then exit with the result code. 1156 raise Match (* Never reached but gives the 'a result [all...] |
H A D | Foreign.581.sml | 80 executed until we actually want the result. *)
|
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | llistScript.sml | 2761 Infinite repetitions of the argument. If it's [], then the result is
|
/seL4-l4v-master/seL4/src/arch/arm/64/kernel/ |
H A D | vspace.c | 2518 readWordFromVSpace_ret_t result; local 2519 result = readWordFromVSpace(vspaceRoot, address); 2520 if (result.status == EXCEPTION_NONE) { 2521 printf("0x%lx: 0x%lx\n", (unsigned long)address, (unsigned long)result.value);
|
/seL4-l4v-master/seL4/src/arch/arm/32/kernel/ |
H A D | vspace.c | 2930 readWordFromVSpace_ret_t result; local 2931 result = readWordFromVSpace(pd, address); 2932 if (result.status == EXCEPTION_NONE) { 2933 printf("0x%lx: 0x%lx\n", (long)address, (long)result.value);
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setScript.sml | 2295 (* Left inverse, to option type, result is NONE outside image of domain *)
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | SharingTables.sml | 137 val (result, strtable', idtable', table') = value 140 (result::results, strtable', idtable', table')
|
/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | errormonad.sml | 68 | Some((s0',s'), result) => Some(s0',(s',result))
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 493 to prove the equivalence of the result via repeated 3542 (* construct exhaustiveness result *)
|