/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/ |
H A D | m0_core_decompLib.sml | 226 val (test_cert, test_def) = m0_core_decompLib.m0_core_decompile "test"` 243 cmp r0, r3 ; test if done 252 eval ``test (T, (\a. if a && 3w = 0w then 4w else 0w), dmem, 255 val test = Count.apply m0_triple value 257 test "D000"; 258 test "D100"; 259 test "D200"; 260 test "D300"; 261 test "D400"; 262 test "D50 [all...] |
/seL4-l4v-master/HOL4/src/1/ |
H A D | ScaledTests.sml | 11 fun average (gen, test) m n = let 15 else recurse (m - 1) (Time.toReal (usr_time test prob) + acc)
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | github462Script.sml | 25 fun test t = function 28 val _ = assert (List.all test o DefnBase.all_terms) eval_defn
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | fracUtils.sml | 47 (* ---------- test cases ---------- * 53 * ---------- test cases ---------- *) 61 (* ---------- test cases ---------- * 66 * ---------- test cases ---------- *) 84 (* ---------- test cases ---------- * 88 * ---------- test cases ---------- *) 126 (* ---------- test cases ---------- * 133 * ---------- test cases ---------- *)
|
H A D | ratUtils.sml | 50 (* ---------- test cases ---------- * 56 * ---------- test cases ---------- *) 67 (* ---------- test cases ---------- * 72 * ---------- test cases ---------- *)
|
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | github115bScript.sml | 5 (* this theory is in the test-case solely to force Holmake to check that the
|
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | parse_complit.c | 78 struct bar test = {f,{1,2},{101}}, test2 = {{1}, {2}, {3}}; local 79 struct bar b_array[10] = { test, test2, 1, 2 };
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlTacticData.sml | 57 fun test call = not (is_local (#stac call)) function 58 val calls2 = filter (test o snd) calls1 66 fun test (x,_,_) = (x = thy) function 67 val calls = filter (test o fst) (dlist (#calld tacdata)) 122 fun test file = exists_file file function 125 val filel = filter test (map f thyl)
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | selftest.sml | 15 fun test s (problem, result) = let function 123 List.all (test (IMAGE_CONV computeLib.EVAL_CONV NO_CONV)) imgtests 125 List.all (test GSPEC_SIMP_CONV) gspec_simp_tests 127 List.all (test MAX_SET_CONV) max_set_tests
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/nullary_tgt/ |
H A D | nullary_tgtScript.sml | 8 val _ = OS.FileSys.chDir "test"
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | testspec.py | 87 test = Test(doc.get("name"), doc.text.strip(), env) 88 return [test] 119 'test': parse_test 177 # Check that test names are unique. 186 "Duplicate test names: %s" % show_names(dups)) 299 # Check test names are unique and dependencies exist. 346 for test in test_info.tests: 348 test.command, test.timeout, test [all...] |
H A D | run_tests.py | 9 # Very simple command-line test runner. 123 ERROR, # Failed to run test at all 143 def run_test(test, status_queue, kill_switch, 148 Run a single test. 161 command = ["bash", "-c", test.command] 172 if os.path.abspath(test.cwd) != os.path.abspath(os.getcwd()): 173 path = " [%s]" % os.path.relpath(test.cwd) 176 print(" command: %s%s" % (test.command, path)) 190 cwd=test.cwd) 192 output = "Exception while running test [all...] |
/seL4-l4v-master/HOL4/src/string/ |
H A D | stringLib.sml | 94 val test = Count.apply (string_EQ_CONV o Term); 96 test`"" = ""`; 97 test`"a" = ""`; 98 test`"" = "a"`; 99 test`"" = "abc"`; 100 test`"abcdefghijklmnopqrstuvwxyz" = "abcdefghijklmnopqrstuvwxyz"`; 101 test`"abcdefghijklmnopqrstuvwxyz" = "abcdefghijklmnopqrstuvwxyzA"`;
|
/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);
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | selftest.sml | 11 val _ = tprint "AC looping (if test appears to hang, it has failed)" 33 (* test bounded simplification *) 37 "Bounded rewrites (if test appears to hang, it has failed)" 44 (* test abbreviations in tactics *) 62 (* test that bounded rewrites get applied to both branches, and also that 79 (* test that being a bounded rewrite overrides detection of loops in 99 (* test that a bounded rewrite on a variable gets a chance to fire at all *) 114 (* test that a bound on a rewrite applies to all derived rewrite theorems *) 129 (* test that congruence rule for conditional expressions is working OK *) 274 fun test ( function 370 fun test (msg, tac, ing, outgs) = function [all...] |
/seL4-l4v-master/HOL4/examples/finite-test-set/ |
H A D | finite_test_setScript.sml | 14 UOK a "test instance" (n1,...,ns) is a valuation such that 18 UOK The main result proved here is that every formula has a test instance. 22 UOK construct the test instance. 25 UOK Rather than a single instance, they show solvability by a finite test set. 26 UOK A "test set" is a set T of instances such that 91 (* A test of expressiveness: Goldbach's conjecture can be represented *) 114 env is a test instance for f [= (qs,p)] if 125 (* Non-constructive definition of test instances *) 179 (* Solvability by test sets (as in the paper) *) 198 (* A test se [all...] |
/seL4-l4v-master/HOL4/examples/AI_TNN/ |
H A D | mleArithData.sml | 68 Creation of training set, validation set and test set and export 89 writel (arithdir ^ "/test") (map f tmltest) 128 val tml' = map fst (List.concat (map import_arithdata ["test","train"])) 149 app export_computefea ["train","test"];
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 95 fun test(inp, expected) = function 109 val _ = app test [ 325 val test = test_conv "PMATCH_CLEANUP_PVARS_CONV" PMATCH_CLEANUP_PVARS_CONV (``PMATCH (x:('b # 'c) option) [ value 334 val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``PMATCH (x,y,z) value 346 val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``case xy of value 351 val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``case (x,y) of value 357 val test = test_conv "PMATCH_INTRO_WILDCARDS_CONV" PMATCH_INTRO_WILDCARDS_CONV (``PMATCH (x,y,z) value 365 val test = test_conv "PMATCH_CLEANUP_CONV" PMATCH_CLEANUP_CONV (``case (SUC x) of value 368 val test = test_conv "PMATCH_CLEANUP_CONV" PMATCH_CLEANUP_CONV (``case (SOME (x:'a),y) of value 376 val test value 381 val test = test_conv "PMATCH_SIMP_COLS_CONV" PMATCH_SIMP_COLS_CONV (``case (SOME x,y) of value 387 val test = test_conv "PMATCH_SIMP_COLS_CONV" PMATCH_SIMP_COLS_CONV (``case (SOME x,y) of value 396 val test = test_conv "PMATCH_REMOVE_FAST_REDUNDANT_CONV" PMATCH_REMOVE_FAST_REDUNDANT_CONV (``case xy of value 407 val test = test_conv "PMATCH_REMOVE_REDUNDANT_CONV" PMATCH_REMOVE_REDUNDANT_CONV (``case xy of value 418 val test = test_conv "PMATCH_REMOVE_FAST_SUBSUMED_CONV true" (PMATCH_REMOVE_FAST_SUBSUMED_CONV true) (``case xy of value 429 val test = test_conv "PMATCH_REMOVE_FAST_SUBSUMED_CONV false" (PMATCH_REMOVE_FAST_SUBSUMED_CONV false) (``case xy of value 441 val test = test_conv "PMATCH_SIMP_CONV" PMATCH_SIMP_CONV value 838 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 847 val test = test_conv "PMATCH_CASE_SPLIT_CONV_HEU colHeu_first_col" (PMATCH_CASE_SPLIT_CONV_HEU colHeu_first_col) (t, SOME value 860 val test = test_conv "PMATCH_CASE_SPLIT_CONV_HEU colHeu_last_col" (PMATCH_CASE_SPLIT_CONV_HEU colHeu_last_col) (t, SOME value 869 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV (t, SOME value 878 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV (t, SOME value 887 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 894 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 897 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 905 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 913 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 920 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 928 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 934 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 941 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 954 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1002 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1007 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1014 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1020 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1055 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1061 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value 1568 val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( value [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sig | 12 translate_to_c generates 3 files: filename.h, filename.c and filename-test.c in the directory dirname. The directory name must end with a "/". The file filename.c contains the main function definitions, filename.h the headers. 14 filename-test.c contains code for testing. It checks for the tests passed in tests automatically and afterwards provides interactive for
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | selftest.sml | 27 fun test (s, exp) = let function 37 val _ = print "\n" before app (ignore o test) [
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/ |
H A D | var_example2.sml | 6 structure test : MutRecTypeInputSig = structure 59 structure test_Def = MutRecTypeFunc (test);
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/coproduct/ |
H A D | selftest.sml | 6 fun hm testname tgts test = 9 if test() then OK() else die "FAILED!")
|
/seL4-l4v-master/HOL4/polyml/mlsource/ |
H A D | BuildExport.sml | 31 val test = List.exists (fn "--intIsIntInf" => true | _ => false) (CommandLine.arguments()) value 32 val () = Initialise.initGlobalEnv{globalTable=globalTable, intIsArbitraryPrecision=test}
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | selftest.sml | 14 fun test (t1,t2) = convtest ("PRETTIFY_CONV "^term_to_string t1, C, t1, t2) function 16 app test [(t1, t1), (mk_abs(p,t1), mk_abs(p,t1)),
|
/seL4-l4v-master/l4v/tools/autocorres/tests/proof-tests/ |
H A D | nested_struct.c | 29 int test(struct point1 *p1, struct point2 *p2) function
|