Searched refs:test (Results 1 - 25 of 348) sorted by last modified time

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODE.sml102 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 DCODEGEN_PARSETREE.sml539 | 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 DMATCH_COMPILER.sml324 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 DEXPORT_PARSETREE.sml194 | 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 DBASE_PARSE_TREE.sml77 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 DCODETREE_SIMPLIFIER.sml177 | 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 DCODETREE_STATIC_LINK_AND_CASES.sml54 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 DCODETREE_FUNCTIONS.sml75 | 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 DOS.sml989 (* If the poll test returns zero then polling is
/seL4-l4v-master/HOL4/src/parse/
H A DOverload.sml382 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 Dselftest.sml171 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 DBasicProvers.sml991 This seems to be an expensive test, especially since the work
/seL4-l4v-master/HOL4/src/1/
H A Dselftest.sml27 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 DcomputeParamScript.sml1806 The test for order: if (m <= ordz k n) exit
/seL4-l4v-master/l4v/tools/autocorres/tools/
H A Drelease.py120 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 Dbuildutils.sml956 (print "Performing self-test...\n";
959 print "Self-test was successful\n"
/seL4-l4v-master/HOL4/src/real/
H A DtranscScript.sml87 (* Show the series for exp converges, using the ratio test *)
125 (* Show by the comparison test that sin and cos converge *)
H A DseqScript.sml1183 (* Now prove the comparison test *)
1326 (* Now prove the ratio test *)
H A Dselftest.sml8 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 Droot.tex104 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 Droot.tex104 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 Dosmemunix.cpp165 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 Dgc_mark_phase.cpp247 bool test = gpTaskFarm->AddWork(&MTGCProcessMarkPointers::MarkPointersTask, marker, obj); local
248 ASSERT(test);
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DMessage.sml3521 (* 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 DX86CODESIG.sml135 | 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 }

Completed in 281 milliseconds

1234567891011>>