/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODE.sml | 102 mkIf(mkBinary(BuiltIns.WordComparison{test=BuiltIns.TestLess, isSigned=true}, 798 This appears to increase the code size but the test should be 801 constant that represents the value). We have to test 912 val test = 924 if test 999 the test code, the injection and the projection functions. *) 1003 have to be applied to the type arguments to yield the actual injection/test/projection 1004 functions. For monotypes the fields contain the injection/test/projection 1043 (* If this was the last or only constructor we don't need to test. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 539 | codeGenerate(Cond {test, thenpt, elsept, thenBreak, elseBreak, ...}, context) = 541 val (testCode, testEnv) = codeGenerate(test, context) 742 | codeGenerate(While {test, body, breakPoint, ...}, context as { debugEnv, ...}) = 744 val (testCode, testEnv) = codeGenerate(test, context) 752 | codeGenerate(c as Case {test, match, ...}, context as { debugEnv, ...}) = 754 applied to the test expression. *) 756 val testCode = codegen (test, context) 1231 (* The old test was "totalArgs = 1", but that's not really
|
H A D | MATCH_COMPILER.sml | 324 here. We need to use the type-specific equality function to test. 1055 We don't need to test this one and we don't use the default. *) 1086 (* If this is the last one there's no need for a test. *) 1110 (* Create any test code to raise the bind exception *) 1113 then [] (* Exhaustive - no test needed. *) 1138 structure for a binding. This does the test separately from loading 1140 since the pattern is taken apart both in the test and for loading. *)
|
H A D | EXPORT_PARSETREE.sml | 194 | Cond{location, test, thenpt, elsept, thenBreak, elseBreak, ...} => 197 [(test, ref NONE), (thenpt, thenBreak), (elsept, elseBreak)] @ commonProps) 442 | While{location, test, body, breakPoint, ...} => 445 [(test, ref NONE), (body, breakPoint)] @ commonProps) 447 | Case{location, test, match, listLocation, expType=ref expType, ...} => 450 fun getExpr () = getExportTree({parent=SOME asParent, previous=NONE, next=SOME getMatches}, test)
|
H A D | BASE_PARSE_TREE.sml | 77 test: parsetree, 180 { test: parsetree, body: parsetree, location: location, breakPoint: breakPoint option ref } 184 { test: parsetree, match: matchtree list, location: location, listLocation: location, expType: types ref }
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 177 | simpGeneral context (Arbitrary{oper=ArbCompare test, shortCond, arg1, arg2, longCall}) = 178 SOME(specialToGeneral(simpArbitraryCompare(test, shortCond, arg1, arg2, longCall, context, RevList []))) 306 | simpGeneral context (TagTest{test, tag, maxTag}) = 308 case simplify(test, context) of 313 | sTest => SOME(TagTest{test=sTest, tag=tag, maxTag=maxTag}) 435 Binary{oper=WordComparison{test=TestEqual, isSigned=false}, 492 | simpSpecial (Arbitrary{oper=ArbCompare test, shortCond, arg1, arg2, longCall}, context, tailDecs) = 493 simpArbitraryCompare(test, shortCond, arg1, arg2, longCall, context, tailDecs) 958 (* We use this to test for nil values and if we have constructed a record 1022 (WordComparison{test, isSigne [all...] |
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 54 test : backendIC, 193 | insert(Arbitrary { oper=ArbCompare test, shortCond, arg1, arg2, longCall}) = 202 BICBinary { oper = BuiltIns.WordComparison{test=test, isSigned=true}, arg1 = arg1, arg2 = arg2 } 452 | insert(TagTest{test, tag, maxTag}) = BICTagTest{test=insert test, tag=tag, maxTag=maxTag} 487 { tag: word, test: codetree, caseType: caseType } option; 512 fun findCase (BICBinary{oper=BuiltIns.WordComparison{test=BuiltIns.TestEqual, ...}, arg1, arg2}) = 518 then SOME{tag=toShort c1, test 672 val test = value [all...] |
H A D | CODETREE_FUNCTIONS.sml | 75 | codeProps (TagTest{ test, ... }) = codeProps test 588 | checkUse isMain (TagTest{test, ...}, cl, _) = checkUse isMain (test, cl -- 1, false)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | OS.sml | 989 (* If the poll test returns zero then polling is
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Overload.sml | 382 fun test ((fvs, pat), (orig, nm, tstamp)) = let function 399 val inst_data = List.mapPartial test matches
|
/seL4-l4v-master/HOL4/src/boss/ |
H A D | selftest.sml | 171 fun test (msg, c) = function 181 val _ = List.app test [("simp", SIMP_CONV (srw_ss()) []), ("EVAL", EVAL)] 267 fun test q = function 281 val _ = require_msg (check_result check_defs) prdefpair test quotation
|
/seL4-l4v-master/HOL4/src/basicProof/ |
H A D | BasicProvers.sml | 991 This seems to be an expensive test, especially since the work
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | selftest.sml | 27 access to the parser (which is implicitly a test of the parser too) *) 37 (* test for the INST_TYPE bug that allows instantiation to cause a 119 fun test f x = f x orelse raise InternalDie function 121 val _ = tprint "Identity of old constants test" 130 val _ = test (fn (c1,c2) => Term.compare(c1, c2) <> EQUAL) (c1, c2) 131 val _ = test (not o uncurry aconv) (c1, c2) 132 val _ = test (not o uncurry aconv) (c1, c3) 133 val _ = test (not o uncurry aconv) (c2, c3) 134 val _ = test (String.isPrefix "old" o #Name o dest_thy_const) c1 135 val _ = test (Strin 454 val test = condprinter_test value 605 fun test (ai,ti) = function 636 fun test s = (save_thm(s, TRUTH); die ("Failed to reject: "^s)) function 1139 fun test (nm, pat, expected) = function [all...] |
/seL4-l4v-master/HOL4/examples/AKS/compute/ |
H A D | computeParamScript.sml | 1806 The test for order: if (m <= ordz k n) exit
|
/seL4-l4v-master/l4v/tools/autocorres/tools/ |
H A D | release.py | 120 parser.add_argument('-t', '--test', action='store_true', default=False, 394 # Run a test if requested. 395 if args.test:
|
/seL4-l4v-master/HOL4/tools/ |
H A D | buildutils.sml | 956 (print "Performing self-test...\n"; 959 print "Self-test was successful\n"
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | transcScript.sml | 87 (* Show the series for exp converges, using the ratio test *) 125 (* Show by the comparison test that sin and cos converge *)
|
H A D | seqScript.sml | 1183 (* Now prove the comparison test *) 1326 (* Now prove the ratio test *)
|
H A D | selftest.sml | 8 fun test (problem, result) = let function 42 val _ = List.app test tests 56 fun test (t1,t2) = (Exn.capture c t1, Exn.capture c t2) function 78 require_msg (check t2) (pr t2) test (t1,t2)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 104 increase the test coverage. This manual also explains how to install the tool on 987 \slshape The type $'a$ passed the monotonicity test; Nitpick might be able to skip 1219 The types $'a$ and $'b$ passed the monotonicity test; Nitpick might be able to skip some scopes. 1251 In theory, it should be sufficient to test a single scope:
|
/seL4-l4v-master/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 104 increase the test coverage. This manual also explains how to install the tool on 987 \slshape The type $'a$ passed the monotonicity test; Nitpick might be able to skip 1219 The types $'a$ and $'b$ passed the monotonicity test; Nitpick might be able to skip some scopes. 1251 In theory, it should be sufficient to test a single scope:
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | osmemunix.cpp | 165 void *test = mmap(0, pageSize, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANON, -1, 0); local 166 if (test != MAP_FAILED) 168 munmap(FIXTYPE test, pageSize); 379 void *test = mmap(0, pageSize, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANON, -1, 0); local 380 if (test != MAP_FAILED) 383 munmap(FIXTYPE test, pageSize); 389 test = mmap(0, pageSize, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANON, -1, 0); 390 if (test == MAP_FAILED) 392 munmap(FIXTYPE test, pageSize);
|
H A D | gc_mark_phase.cpp | 247 bool test = gpTaskFarm->AddWork(&MTGCProcessMarkPointers::MarkPointersTask, marker, obj); local 248 ASSERT(test);
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Message.sml | 3521 (* This message is used to test if we are using the Poly callback. We use
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86CODESIG.sml | 135 | ConditionalBranch of { test: branchOps, label: label } 136 | SetCondition of { output: genReg, test: branchOps } 185 | CondMove of { test: branchOps, output: genReg, source: genReg regOrMemoryArg, opSize: opSize }
|