/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/decompiler/ |
H A D | x64_decompLib.sml | 72 val (text_cert, test_def) = x64_decompile_code "test" `add rax, rbx`
|
/seL4-l4v-master/HOL4/src/num/theories/ |
H A D | selftest.sml | 112 val _ = tprint ("dot test: "^term_to_string t)
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | tactics.sig | 41 val test : ('a -> 'b) -> 'a -> 'a value
|
/seL4-l4v-master/HOL4/tools/ |
H A D | build.sml | 84 print ("Self-test directory "^src^" built successfully.\n")
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_equalScript.sml | 23 (* 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 D | modelCheck.sml | 9 open modelCheckLib; (* thus this test is Moscow ML only *)
|
/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/graph-refine/ |
H A D | logic.py | 1391 (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 D | trace_refute.py | 264 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 D | String.sml | 460 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 D | arm8AssemblerLib.sml | 315 fun test n = function 339 (test 100000; !examine)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | envTools.sml | 35 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 D | UnclockedSemanticsScript.sml | 192 * 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 D | many_local_vars.c | 7 int test(void) { function
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | selftest.sml | 232 fun test (msg, g) = function 241 app (ignore o test) [
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | hhTranslate.sml | 125 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 D | BackendIntermediateCodeSig.sml | 62 test : backendIC, 88 | BICTagTest of { test: backendIC, tag: word, maxTag: word }
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/ |
H A D | mips_stepLib.sml | 1201 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 D | arm_stepLib.sml | 1252 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 D | normalForms.sml | 1526 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 D | mklrtable.sml | 375 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 D | x86_Lib.sml | 198 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 D | selftest.sml | 71 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 D | TYPECHECK_PARSETREE.sml | 812 | 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 D | test.sml | 57 (* Example datatypes to test boolification. *)
|