Searched refs:trace (Results 76 - 100 of 260) sorted by relevance

1234567891011

/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttExec.sml164 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 Dlogic.py20 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 Dcheck.py17 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 Ddebug.py380 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 Dproblem.py13 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 Dsyntax.py12 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 Dstack_logic.py17 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 DMakefile.common154 ${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 Dppc_decoderScript.sml169 { 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 DctlCheck.sml80 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 Dselftest.sml7 val _ = QbfTrace.trace := 0
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DsatConfig.sml21 proof : string option, (* proof trace file in HolSatLib format; overrides solver if SOME*)
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmetisTools.sig9 (* "Metis" trace levels:
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DTrace.sml28 fun trace x = (!trace_hook) x function
H A DTraverse.sml88 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 DLibrary.sml20 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 DskiTools.sml30 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 DRewrite.sml209 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 DRule.sml164 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 DRewrite.sml209 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 DRule.sml164 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 DBoolExtractShared.sml377 trace = 2,
382 trace = 2,
387 trace = 2,
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/
H A DreductionEval.sml144 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 Dmachine_ieeeScript.sml76 (Controlled by the trace "native IEEE". Off by default.)
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DintReduce.sml66 key = SOME([], pat), trace = 2,

Completed in 321 milliseconds

1234567891011