Searched refs:test (Results 126 - 150 of 348) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/decompiler/
H A Dx64_decompLib.sml72 val (text_cert, test_def) = x64_decompile_code "test" `add rax, rbx`
/seL4-l4v-master/HOL4/src/num/theories/
H A Dselftest.sml112 val _ = tprint ("dot test: "^term_to_string t)
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dtactics.sig41 val test : ('a -> 'b) -> 'a -> 'a value
/seL4-l4v-master/HOL4/tools/
H A Dbuild.sml84 print ("Self-test directory "^src^" built successfully.\n")
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_equalScript.sml23 (* equality test - main loop
38 test r8,1
40 test r9,1
61 (* equality test *)
/seL4-l4v-master/HOL4/examples/temporal_deep/src/examples/
H A DmodelCheck.sml9 open modelCheckLib; (* thus this test is Moscow ML only *)
/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/graph-refine/
H A Dlogic.py1391 (kind, ns, test, unvisited) = cycle[i]
1434 for (kind, ns, test, unvisited) in cycle:
1435 if test and subgraph_test (ns):
1661 def binary_search_least (test, minimum, maximum):
1662 """find least n, minimum <= n <= maximum, for which test (n)."""
1664 if test (minimum):
1666 if maximum == minimum or not test (maximum):
1670 if test (cur):
1677 def binary_search_greatest (test, minimum, maximum):
1678 """find greatest n, minimum <= n <= maximum, for which test (
[all...]
H A Dtrace_refute.py264 def test (call_hyps, vis_pcs): function in function:refute_minimise_vis_hyps
269 if not test (call_hyps, vis_pcs):
274 if test (call_hyps [ - i : ], vis_pcs2):
282 if not test (call_hyps, kept + vis_pcs[i + 1 :]):
/seL4-l4v-master/HOL4/polyml/basis/
H A DString.sml460 val test = RunCall.byteVectorCompare(s1, s2, wordSize, wordSize, if s1l < s2l then s1l else s2l) value
462 if test = 0 (* If the strings are the same up to the shorter length ... *)
464 else test
484 val test = RunCall.byteVectorCompare(s1, s2, wordSize, wordSize, if s1l < s2l then s1l else s2l) value
486 if test = 0
488 else test >= 0
495 val test = RunCall.byteVectorCompare(s1, s2, wordSize, wordSize, if s1l < s2l then s1l else s2l) value
497 if test = 0
499 else test <= 0
506 val test value
517 val test = RunCall.byteVectorCompare(s1, s2, wordSize, wordSize, if s1l < s2l then s1l else s2l) value
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/
H A Darm8AssemblerLib.sml315 fun test n = function
339 (test 100000; !examine)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DenvTools.sml35 fun dest_env ie = let val (test,x,ie2) = dest_cond(body(snd(dest_eq(concl(ONCE_REWRITE_CONV [ENV_UPDATE_def] ie))))) value
36 in (fst (dest_comb ie2),(snd(dest_eq test),x)) end
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/
H A DUnclockedSemanticsScript.sml192 * LESS m is predicate to test if a number is less than m
194 * LESSX m is predicate to test if a number is less than extended number m
/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dmany_local_vars.c7 int test(void) { function
/seL4-l4v-master/HOL4/src/num/arith/src/
H A Dselftest.sml232 fun test (msg, g) = function
241 app (ignore o test) [
/seL4-l4v-master/HOL4/src/holyhammer/
H A DhhTranslate.sml125 fun test x = must_pred x orelse is_abs x function
126 val subtm = find_term test tm
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCodeSig.sml62 test : backendIC,
88 | BICTagTest of { test: backendIC, tag: word, maxTag: word }
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/
H A Dmips_stepLib.sml1201 fun test s = step (Redblackmap.find (mips_dict, s))
1202 fun test s = (Redblackmap.find (mips_dict, s))
1204 val v = test "ADDI";
1205 val v = test "ADDU";
1206 val v = test "J";
1207 val v = test "BEQ";
1208 val v = test "BEQL";
1209 val v = test "BLTZAL";
1210 val v = test "BLTZALL";
1211 val v = test "ERE
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_stepLib.sml1252 fun test opt s = arm_step opt (arm_encode_from_string s);
1253 test "" "svc #4";
1254 test "" "adds r1, r2";
1255 test "" "ldrex r1,[r2]";
1257 val test = arm_step "fiq";
1258 val _ = test "0xE591F000"; (* ldr pc,[r1] *)
1259 val _ = test "0xF8110A00"; (* rfeda r1 *)
/seL4-l4v-master/HOL4/src/metis/
H A DnormalForms.sml1526 fun test n = ((time DEF_CNF_CONV' o time (mk_neg o var_pigeon)) n; n); function
1528 test 8;
1529 test 9;
1530 test 10;
1531 test 11;
1532 test 12;
1533 test 13;
1534 test 14;
1535 test 15;
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dmklrtable.sml375 val test = fn REDUCE i => update(ruleReduced,i,true) value
378 (app (fn (_,r) => test r) actions;
379 test default)
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_Lib.sml198 val th = x86_step "F7C638000000"; (* test esi,56 *)
199 val th = x86_step "F70337020000"; (* test dword [ebx],567 *)
200 val th = x86_step "850B"; (* test [ebx], ecx *)
/seL4-l4v-master/HOL4/src/n-bit/
H A Dselftest.sml71 fun test (c:conv) tm = function
145 val blast_true = test blastLib.BBLAST_PROVE
148 val srw_true = test (simpLib.SIMP_PROVE (srw_ss()) [])
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DTYPECHECK_PARSETREE.sml812 | Cond {test, thenpt, elsept, location, ...} =>
814 (* The test must be bool, and the then and else parts must be the
817 val testType = assValues v test;
825 valTypeMessage (lex, typeEnv) ("If:", test, testType),
1333 | While {test, body, location, ...} =>
1335 val testType = assValues v test
1342 valTypeMessage (lex, typeEnv) ("While:", test, testType),
1348 | aCase as Case {test, match, location, expType, ...} =>
1353 val argType = assValues aCase test;
1354 (* The matches constitute a function from the test typ
[all...]
/seL4-l4v-master/HOL4/src/Boolify/test/
H A Dtest.sml57 (* Example datatypes to test boolification. *)

Completed in 207 milliseconds

1234567891011>>