/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | elf_parser.py | 52 header = re.search('kernel\.elf:\s*file\s*format\s*elf32-littlearm',line) 53 header2 = re.search('Disassembly of section \..*:',line) 57 ndks = re.search('.*ndks_boot.*',line) 63 r = re.search('(?P<f_addr>.*) <(?P<f_name>.*)>:$',line) 80 literal = re.search('(?P<addr>.*):\s*[a-f0-9]+\s*(?P<size>(\.word)|(\.short)|(\.byte))\s*(?P<value>0x[a-f0-9]+)$',line) 92 match = re.search('(?P<line_addr>.*):.*',line) 107 match = re.search(r'[a-f0-9]+:\s*[a-f0-9]+\s+(b|bx)\s+.*',inst)
|
H A D | cplex.py | 70 if re.search(unbounded,line) or re.search(infeasible, line): 74 match = re.search(objective_regex,line) 87 if re.search(r'^End',line):
|
H A D | elf_file.py | 59 match = re.search('(.*)(_clone).*',f) 112 match = re.search(r'^.*:\s+(?P<raw>[a-f0-9]+)\s*(?P<text>.*)$',inst)
|
H A D | bench.py | 131 if s.startswith('Loop') or re.search(r'\s*\(=',s) or re.search(r'\s*\(',s):
|
H A D | conflict.py | 362 match = re.search(r'\s*\[(?P<infeas>.*)\]\s*:\s*(?P<kind>.*$)', line) 402 match = re.search(r'.*:\s*(?P<kind>.*$)', line) 410 match = re.search(r'\[(?P<addr>.*)\]:(?P<kind>.*$)', line) 413 match = re.search(r'\s*\[(?P<addr>.*)\]\s*:\s*\[(?P<times>.*)\]\s*:\s*(?P<kind>.*$)', line)
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibSimple.sig | 35 - ty : search a guess for either universal or existential quantification 36 - v : variable to search an instance for 37 - tm : a term to search an instantiation in 49 Having an additional callback argument to search guesses for subterms is also useful. 50 combine_sgsfwcs then allows combining a list of such search functions with callback 51 into a single search function. 60 (* search functions for common operations *) 86 (* Generalised conversions that allow specifying which search functions to use *)
|
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | mesonLib.sig | 2 (* Version of the MESON procedure a la PTTP. Various search options. *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibMetis.sig | 11 1: Status information during proof search 14 4: High-level proof search information 15 5: Log of every inference during proof search
|
H A D | mlibMetis.sml | 28 1: Status information during proof search 31 4: High-level proof search information 32 5: Log of every inference during proof search
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stats.py | 9 import search namespace 63 nec = search.get_necessary_split_opts (p, loop_head, 92 va = search.get_loop_var_analysis_at (p, loop_head) 119 i_j_opts = search.mk_i_j_opts (unfold_limit = window_size) 121 knowledge = search.setup_split_search (rep, loop_head, restrs, hyps, 124 res = search.split_search (loop_head, knowledge) 137 if not search.mk_i_j_opts (unfold_limit = i):
|
H A D | debug.py | 16 import search namespace 118 if search.eval_model_expr (m, rep.solv, 154 r = search.eval_model (m, x) 343 v = search.eval_model (m, sx) 367 v = search.eval_model_expr (m, solv, expr) 503 offs = search.eval_model_expr (m, rep.solv, offs) 508 data = [(addr, search.eval_model_expr (m, rep.solv, 550 ev = search.eval_model (m, s_x) 689 proof = search.last_proof[0] 700 proof = search [all...] |
H A D | loop_bounds.py | 1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace 8 from search import eval_model_expr 30 """performs a binary search between minimum and maximum, but does not start 71 #naive binary search to find loop bounds 105 #do a downward binary search to find the concrete loop bound 185 standard = set (search.mk_seq_eqs (p, split, 1, with_rodata = False)) 189 cands = search.mk_seq_eqs (p, split, 1, with_rodata = False) 223 standard = set (search.mk_seq_eqs (p, split, 1, with_rodata = False)) 258 vas = search.get_loop_var_analysis_at(p, split) 486 if len (search [all...] |
H A D | graph-refine.py | 18 import search namespace 71 proof = search.build_proof (p) 94 except search.NoSplit: 97 printout ('Solver timeout/failure in proof search.')
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttSearch.sig | 25 val search : value
|
H A D | tttSetup.sig | 37 (* search *)
|
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/stats/ |
H A D | summary.py | 20 m = re.search(r, str)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Subsume.sml | 186 fun search [] = NONE function 187 | search ((sub,[]) :: others) = 191 if pred x then SOME x else search others 193 | search ((_, [] :: _) :: others) = search others 194 | search ((sub, (sub' :: subs) :: subsl) :: others) = 199 NONE => search others 200 | SOME sub => search ((sub,subsl) :: others) 205 | SOME sub_subsl => search [sub_subsl]
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subsume.sml | 186 fun search [] = NONE function 187 | search ((sub,[]) :: others) = 191 if pred x then SOME x else search others 193 | search ((_, [] :: _) :: others) = search others 194 | search ((sub, (sub' :: subs) :: subsl) :: others) = 199 NONE => search others 200 | SOME sub => search ((sub,subsl) :: others) 205 | SOME sub_subsl => search [sub_subsl]
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Help.sig | 36 /str cyclically search for string str in help file (case-insensitive) 37 n search for next occurrence of str 51 records, each of which maps a search term to the specified file
|
H A D | Help.sml | 28 The browser's search facility cyclically searches (case-insensitive) 41 (* Additional directories to search for help files *) 79 (* Mapping particular search terms to non-.sig files: *) 151 fun search chars = function 156 NONE => (print "**** No previous search string\n"; 170 | SOME (#"/" :: s) => search s 289 (* Main help function: search for a string in the signature index database: *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | match_goal.sml | 144 fun search [] d = try_tactic d function 145 | search (m::ms) d = stream_flat (stream_map (search ms) (m d)) 151 (case search matches (empty_named_thms,empty_named_tms) () of
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | HM_DepGraph.sml | 147 fun search i = function 151 if #status nI <> Pending then search (i + 1) 153 else search (i + 1) 155 search 0
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernel.sml | 262 * the search failed because the sought-for subterm is not there, or because * 287 fun search bvs actions = function 290 | POP :: alist => search (tl bvs) alist 296 COMB (t1, t2) => search bvs (SEARCH t1 :: SEARCH t2 :: alist) 297 | LAMB (bv, t) => search (bv :: bvs) (SEARCH t :: POP :: alist) 298 | _ => search bvs alist 300 search [] [SEARCH t] 304 fun search bvs actions acc = function 307 | POP :: alist => search (tl bvs) alist acc 314 COMB(t1, t2) => search bv [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/ |
H A D | description.tex | 81 help\index{help!updating search path} search path. The help search path is 83 library. After updating the help search path, the \ml{reduce} 95 Updating help search path 97 Extending help search path.
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | combin.tex | 140 Meson search level: ... 304 Meson search level: ......... 328 Meson search level: .......... 503 Meson search level: ..... 525 Meson search level: ............ 549 Meson search level: ....... 631 Meson search level: ... 653 Meson search level: ............ 682 Meson search level: ....... 835 Meson search leve [all...] |