| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | threads.tex | 192 Debug exceptions are used to deliver trace and debug related events to threads.
193 Breakpoints, watchpoints, trace-events and instruction-performance sampling
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 250 trace = 10}],
254 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) };
1121 trace = 2, key = SOME ([],``address$ALIGNED a``),
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 143 The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e.\ it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.
355 Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 143 The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e. it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.
355 Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cearTools.sml | 526 (* check whether abstract counterexample atr has concrete counterpart upto nth state of the abstract counterexample trace*)
584 then NONE (*FIXME: fix TRUTH below so we can recover a concrete trace from it*)
598 val ctr = if isSome satth andalso is_imp (concl (valOf satth))(* return concrete trace if one was found else NONE *)
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | Useful.sml | 127 fun trace message = !trace_print message; function
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | EnumType.sml | 344 trace = 2,
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
| H A D | RecordType.sml | 161 val save_thm = Feedback.trace ("Theory.save_thm_reporting", 0) save_thm
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | folTools.sml | 37 fun chat s = (trace s; true)
|
| H A D | mlibClause.sml | 38 fun chat s = (trace s; true)
|
| H A D | mlibClauseset.sml | 40 fun chat s = (trace s; true)
|
| H A D | mlibMeson.sml | 33 fun chat s = (trace s; true)
|
| H A D | mlibModel.sml | 26 fun chat s = (trace s; true)
|
| H A D | mlibThm.sml | 29 fun chat s = (trace s; true)
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | fcpScript.sml | 16 val qDefine = Feedback.trace ("Define.storage_message", 0) zDefine
|
| /seL4-l4v-10.1.1/HOL4/src/num/termination/ |
| H A D | TotalDefn.sml | 612 trace ("show_typecheck_errors", 0)
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | type_grammar.sml | 418 (Feedback.trace ("print_tyabbrevs", 0) (pp_type G))
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sig | 44 val chatting : bool ref (* default is false, no trace of quotient operation *)
|
| /seL4-l4v-10.1.1/HOL4/src/refute/ |
| H A D | Canon.sml | 558 let (* val _ = trace (1,"refute -- ",tm) *)
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
| H A D | binderLib.sml | 19 |> trace ("Unicode", 0)
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
| H A D | milawa_coreScript.sml | 356 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) };
|
| /seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
| H A D | quick.tex | 279 \hol{Feedback}{set_trace} \var{name} \var{int} & set a tracing level for a registered trace \\
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | selftest.sml | 36 val t2s = trace ("types",2) term_to_string
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/TWOFISH/ |
| H A D | twofishScript.sml | 464 {name="PBETA",trace = 3,conv=K (K PairRules.PBETA_CONV),
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 68 fun trace mesg = !tracePrint mesg; function
|