/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | interpret.cpp | 85 #define arg1 (pc[0] + pc[1]*256) macro 346 pc += arg1 + 2; break; 378 *(--sp) = PolyWord::FromCodePtr(pc + arg1 + 2); /* Address of handler */ 423 pc += arg1 + 2; 447 pc += arg1 + 2; 453 // arg1 is the largest value that is in the range 455 if (u > arg1 || u < 0) pc += (arg1+2)*2; /* Out of range */ 464 // arg1 is the number of cases i.e. one more than the largest value 468 if (u >= arg1 || [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 157 | BICUnary of {oper: BuiltIns.unaryOps, arg1: backendIC} 158 | BICBinary of {oper: BuiltIns.binaryOps, arg1: backendIC, arg2: backendIC} 161 {oper: BuiltIns.arithmeticOperations, shortCond: backendIC, arg1: backendIC, arg2: backendIC, longCall: backendIC} 378 | BICUnary { oper, arg1 } => 380 [ PrettyString(BuiltIns.unaryRepr oper), PrettyBreak(1, 0), printList("", [arg1], ",") ] 383 | BICBinary { oper, arg1, arg2 } => 385 [ PrettyString(BuiltIns.binaryRepr oper), PrettyBreak(1, 0), printList("", [arg1, arg2], ",") ] 388 | BICArbitrary { oper, shortCond, arg1, arg2, longCall } => 391 printList("", [shortCond, arg1, arg2, longCall], ",") ]
|
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 189 | insert(Unary { oper, arg1 }) = BICUnary { oper = oper, arg1 = insert arg1 } 191 | insert(Binary { oper, arg1, arg2 }) = BICBinary { oper = oper, arg1 = insert arg1, arg2 = insert arg2 } 193 | insert(Arbitrary { oper=ArbCompare test, shortCond, arg1, arg2, longCall}) = 195 val insArg1 = insert arg1 and insArg2 = insert arg2 199 fun fixedComp(arg1, arg2) = 200 BICBinary { oper = BuiltIns.WordComparison{test=test, isSigned=true}, arg1 [all...] |
H A D | BackendIntermediateCodeSig.sml | 48 | BICUnary of {oper: BuiltIns.unaryOps, arg1: backendIC} 49 | BICBinary of {oper: BuiltIns.binaryOps, arg1: backendIC, arg2: backendIC} 51 | BICArbitrary of {oper: BuiltIns.arithmeticOperations, shortCond: backendIC, arg1: backendIC, arg2: backendIC, longCall: backendIC}
|
H A D | BaseCodeTreeSig.sml | 83 | Unary of {oper: BuiltIns.unaryOps, arg1: codetree} 84 | Binary of {oper: BuiltIns.binaryOps, arg1: codetree, arg2: codetree} 91 {oper: arbPrecisionOps, shortCond: codetree, arg1: codetree, arg2: codetree, longCall: codetree}
|
H A D | CODETREE_FUNCTIONS.sml | 99 | codeProps (Unary{oper, arg1}) = 122 operProps andb codeProps arg1 125 | codeProps (Binary{oper, arg1, arg2}) = 147 operProps andb codeProps arg1 andb codeProps arg2 150 | codeProps (Arbitrary{shortCond, arg1, arg2, longCall, ...}) = 154 codeProps shortCond andb codeProps arg1 andb codeProps arg2 andb codeProps longCall
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Arith_cons.sig | 40 val arg1 : term -> term value
|
H A D | Arith_cons.sml | 129 val arg1 = rand o rator value
|
H A D | Gen_arith.sml | 45 ((let val b = contains_var' (arg1 tm) 51 ((contains_var' (arg1 tm)) orelse (contains_var' (arg2 tm))) 97 then Lib.union (non_presburger_subterms (arg1 tm))
|
H A D | Norm_arith.sml | 46 (if ((is_plus tm) andalso (is_num_const (arg1 tm))) 47 then if ((is_plus (arg2 tm)) andalso (is_num_const (arg1 (arg2 tm)))) then 219 (is_num_const (arg1 tm')) andalso 276 (is_num_const (arg1 tm2)) andalso 408 (let val tm2' = arg1 tm2
|
H A D | Norm_bool.sml | 89 (if ((is_disj tm) andalso (is_disj (arg1 tm)))
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | separationLogicSyntax.sml | 252 val (arg1, arg2) = strip_comb_2 asl_exists_list_term tt; value 254 (arg1,arg2) 330 val (arg1, arg2) = (el 1 args, el 2 args); value 351 (op_term, arg1, arg2, def_thm)
|
H A D | vars_as_resourceSyntax.sml | 114 val (arg1, arg2) = (el 1 args, el 2 args); value 115 val (v, t') = dest_abs arg1; 122 val arg1 = el 1 args; value 123 val (v, t') = dest_abs arg1;
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/frv/ |
H A D | ffi.c | 166 void ffi_closure_eabi (unsigned arg1, unsigned arg2, unsigned arg3, argument 182 { arg1, arg2, arg3, arg4, arg5, arg6 };
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibArbnum.sml | 379 fun test_op (nf, origf, P, print_opn, testresult) arg1 arg2 = let 380 val _ = P (arg1, arg2) orelse raise ArgsBad 381 val orig_result = origf(arg1, arg2) 382 val new_result = nf(fromInt arg1, fromInt arg2) 385 print (Int.toString arg1^print_opn^Int.toString arg2); 394 val arg1 = range (0, 60000000) gen 397 test_op opdetails arg1 arg2
|
H A D | mlibClause.sml | 672 fun RESOLVE arg1 arg2 = 673 if not (chatting 1) then RESOLVE' arg1 arg2 else 677 PP.pp_to_string 70 (pp_pair pp_clause pp_int) arg1 ^ "\n" ^ 681 RESOLVE' arg1 arg2 721 fun PARAMODULATE arg1 arg2 = 722 if not (chatting 1) then PARAMODULATE' arg1 arg2 else 726 PP.pp_to_string 70 (pp_triple pp_clause pp_int pp_bool) arg1 ^ "\n"^ 730 PARAMODULATE' arg1 arg2
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/pa/ |
H A D | hpux32.S | 88 %arg1(ecif) -- same as incoming param 99 ldw -40(%sp), %arg1 284 stw %arg1, -40(%r3) 290 copy %r3, %arg1
|
H A D | linux.S | 82 %arg1(ecif) -- same as incoming param 93 ldw -40(%sp), %arg1 276 stw %arg1, -40(%r3) 282 copy %r3, %arg1
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | ReadHMF.sml | 146 val (arg1, arg2) = value 163 val (arg1, s) = read_quoted_string b s value 168 (arg1, arg2) 170 val (q1, q2) = (extract_normal_quotation (ss arg1),
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/machine/ |
H A D | l2c_310.c | 235 mshield_smc(uint32_t callid, uint32_t arg1, uint32_t arg2) argument 237 register uint32_t _arg1 asm ("r0") = arg1;
|
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
H A D | Arbnumcore.sml | 494 fun test_op (nf, origf, P, print_opn, testresult) arg1 arg2 = let 495 val _ = P (arg1, arg2) orelse raise ArgsBad 496 val orig_result = origf(arg1, arg2) 497 val new_result = nf(fromInt arg1, fromInt arg2) 500 print (Int.toString arg1^print_opn^Int.toString arg2); 509 val arg1 = range (0, 60000000) gen 512 test_op opdetails arg1 arg2
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODE.sml | 62 val arg1 = mkLoadArgument 0 (* Used frequently. *) value 187 [arg1]), 234 | (FunctionType{arg=arg1, result=result1}, FunctionType{arg=arg2, result=result2}) => 235 sameType(arg1, arg2) andalso sameType(result1, result2) 514 [arg1]), 524 [arg1]), 535 val entryCode = mkEval(printCode(typeof, localLevel), [arg1]) 553 val valToPrint = mkInd(0, arg1) and depthCode = mkInd(1, arg1) 711 mkEval(compareElements, [mkInd(n, arg1), mkIn [all...] |
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 31 "c:/program files/bar/baz" "arg1"
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | problem-set-1-answers.lisp | 309 ; Define opcode to take an instruction and return the op. Define arg1, arg2, 316 (defun arg1 (inst) (nth 1 inst)) function
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | type_pp.sml | 231 | [arg1, arg2] => 261 pr_ty arg1 (Lfx (prec, printthis)) (depth - 1) >>
|