/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttExec.sml | 164 val (TC_OFF : tactic -> tactic) = trace ("show_typecheck_errors", 0) 171 timeOut tim (trace ("show_typecheck_errors", 0) tac) g
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | logic.py | 20 from target_objects import trace, printout namespace 367 trace ('no accumulator %s' % ((expr, nm, typ), )) 798 trace = None): 837 if trace != None: 838 trace[0] = (direct_costs, future_costs, prev_costs, 843 trace = None): 880 if trace and n in trace: 935 trace ('warmup overrun in compute_var_cycle_analysis') 936 trace ('chasin [all...] |
H A D | check.py | 17 from target_objects import functions, pairings, trace, printout namespace 43 trace ('Done inlining.') 64 [trace ('Skipped inlining underspecified %s.' 68 trace ('Function %s at %d - %s - completely unmatched.' 123 trace ('Skipping inlining underspecified %s' % f_nm) 744 trace ('Testing group of hyps: %s' % list (names), push = 1) 746 trace ('Group result: %r' % res, push = -1) 785 trace ('%s: proof failed!' % name) 786 trace (' (failure kind: %r)' % detail[0]) 949 trace ('loadin [all...] |
H A D | debug.py | 380 trace = [] 420 trace.extend ([(kind, addr, v, mem, n, vc) 425 trace.append (msg) 426 return trace 452 print '%s mem trace:' % tag 540 trace = [] 567 trace.append (((n, vc), val)) 575 trace.append (msg) 576 return trace
|
H A D | problem.py | 13 from target_objects import functions, pairings, trace, printout namespace 181 trace ('Loop (%d, %s)' % (head, tail)) 725 trace ('Inlining %s into %s' % (f_nm, p.name)) 727 trace (' inlining into loop %d!' % p.loop_id (n)) 745 trace ('Problem size now %d' % len(p.nodes)) 784 trace (' sub-loops %s of loop at %s' % (subs, head)) 786 trace (' head %d tagged %s' % (h, p.node_tags[h])) 838 trace ('Loop vars at head: %s' % loop_vs)
|
H A D | syntax.py | 12 from target_objects import structs, trace namespace 1108 trace ('Loading syntax from %s' % lines.name) 1110 trace ('Loading syntax (from anonymous source).') 1169 trace ('Loaded %d functions, %d structs, %d globals.' 1269 trace ('Missing nodes after calls to %s' % call) 1270 trace (' in %s' % str (sites)) 1273 trace ('Warning: dead arc in %s: %s -> %s' 1275 trace (' (follows %s node!)' % fun.nodes[n].kind) 1282 trace ('Checking %s' % f)
|
H A D | stack_logic.py | 17 from target_objects import functions, trace, pairings, pre_pairings, printout namespace 144 trace ('offs_expr_const: not const') 145 trace ('%s - %s' % (addr_expr, sp_expr)) 146 trace (str (vs)) 147 trace (str (hyps)) 223 trace ('get_ptr_offs fallthrough at %d: %s' % v) 224 trace (str ([hyp] + hyps)) 629 trace ('Inlining %s at %d.' % (p.nodes[n].fname, n)) 798 trace ('todo length %d' % len (todo)) 799 trace ('tai [all...] |
/seL4-l4v-10.1.1/graph-refine/seL4-example/ |
H A D | Makefile.common | 154 ${GRAPH_REFINE} . trace-to:partial-$@ deps:Kernel_C.cancelAllIPC 158 ${GRAPH_REFINE} . trace-to:partial-$@ all
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_decoderScript.sml | 169 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 171 val if_ss = conv_ss { name = "if", trace = 3,
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctlCheck.sml | 80 val ((tb,resthm,trace),(aic,cc)) = absCheck I1 [(".",#6(valOf(#ks(ic))))] state Ric vm ksname (#abs(ic),cc) (nf,mf) (apl,apsubs) 91 in ((tb2,resthm2,trace), ({ks= #ks(ic),th = #th(ic), abs=aic},cc)) end
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | selftest.sml | 7 val _ = QbfTrace.trace := 0
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | satConfig.sml | 21 proof : string option, (* proof trace file in HolSatLib format; overrides solver if SOME*)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | metisTools.sig | 9 (* "Metis" trace levels:
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Trace.sml | 28 fun trace x = (!trace_hook) x function
|
H A D | Traverse.sml | 88 val _ = map (fn thm => trace(2,MORE_CONTEXT thm)) thms 225 (trace(2,TEXT "Limit exhausted"); 290 (trace(4,REDUCE ("Reducing",tm)); conv tm)
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Library.sml | 20 val trace = ref 2 value 22 val _ = Feedback.register_trace ("HolSmtLib", trace, 4) 128 if !trace > 2 then
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | skiTools.sml | 30 fun trace _ _ = (); function 194 trace "vterm_to_ski_patterns: ((vars, tm), res)" 276 val _ = trace
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rewrite.sml | 209 val () = Print.trace pp "Rewrite.add: result" rw 403 val () = Print.trace Thm.pp "Rewrite.rewriteIdRule': th" th 407 val () = Print.trace Thm.pp "Rewrite.rewriteIdRule': result" result 600 val () = Print.trace ppPl "Rewrite.rebuild: rpl" rpl 601 val () = Print.trace ppPl "Rewrite.rebuild: spl" spl 644 val () = Print.trace pp "Rewrite.reduce': rw" rw 650 val () = Print.trace ppResult "Rewrite.reduce': result" result
|
H A D | Rule.sml | 164 val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^ 170 (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); 759 val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl 766 val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges 767 val () = Print.trace ppEdges "Rule.factor': edges" edges 772 val () = Print.trace ppResult "Rule.factor': result" result
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rewrite.sml | 209 val () = Print.trace pp "Rewrite.add: result" rw 403 val () = Print.trace Thm.pp "Rewrite.rewriteIdRule': th" th 407 val () = Print.trace Thm.pp "Rewrite.rewriteIdRule': result" result 600 val () = Print.trace ppPl "Rewrite.rebuild: rpl" rpl 601 val () = Print.trace ppPl "Rewrite.rebuild: spl" spl 644 val () = Print.trace pp "Rewrite.reduce': rw" rw 650 val () = Print.trace ppResult "Rewrite.reduce': result" result
|
H A D | Rule.sml | 164 val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^ 170 (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); 759 val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl 766 val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges 767 val () = Print.trace ppEdges "Rule.factor': edges" edges 772 val () = Print.trace ppResult "Rule.factor': result" result
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | BoolExtractShared.sml | 377 trace = 2, 382 trace = 2, 387 trace = 2,
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
H A D | reductionEval.sml | 144 val _ = Trace.trace (2, Trace.LZ_TEXT (fn () => "Attempting no1 on "^ 262 name = "nopath_CONV", trace = 2}, 265 name = "noreduct_CONV", trace = 2}],
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | machine_ieeeScript.sml | 76 (Controlled by the trace "native IEEE". Off by default.)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | intReduce.sml | 66 key = SOME([], pat), trace = 2,
|