/seL4-l4v-master/seL4/manual/ |
H A D | Makefile | 270 Error = '^! ' macro 298 ${Q}$(LaTeX) $< >.log || if egrep -q $(Error) $*.log ; then cat .log; rm $@; false ; fi
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Unix.sml | 98 then raise OS.SysErr(OS.errorMsg Error.acces, SOME Error.acces)
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMinimize.sml | 166 | _ => (debug "Error: minimize"; raise ERR "minimize" stac) 210 | _ => (debug "Error: prettification or minimization failed"; p)
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | switching_lemma_helperScript.sml | 949 (f s = Error e) ��� 950 ((f >>= g) s = Error e)``, 1006 /\ ~(f s = Error e) 1016 (f s = Error e) ==> 1017 ((f >>= g) s = Error e) 1041 (?e .((f >>= H) s1 = Error e) 1043 ((f >>= H) s2 = Error e)))
|
H A D | switching_lemmaScript.sml | 519 ���e. (comp s1 = Error e) ��� (comp s2 = Error e)``, 1043 (?e. (f2 s1 =Error e) /\ (f2 s2 = Error e))) 1086 (?e. (f2 s1 = Error e) /\ (f2 s2 = Error e) )) 1133 (?e. (f2 s1 = Error e) /\ (f2 s2 = Error e) ))``, 1174 (? e. (f s1=Error e) /\ (f s2 = Error [all...] |
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTermorder.sml | 141 if inconsistent_eqn eqn then raise Error "good_eqn: inconsistent" 283 else raise Error "add_leq: direct contradiction") 298 | Greater => raise Error "add_leq: violates order (weight)"
|
H A D | mlibSubsume.sml | 53 val () = assert (x <> y) (Error "psym: refl")
|
H A D | mlibSolver.sml | 72 (assert (is_contradiction th) (Error "contradiction_solver: thm not |- F"); 109 handle Error _ => raise Bug "advance: shouldn't fail";
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex.sml | 129 | _ => (report_error ("Error while parsing '"^filename^ 131 | _ => (report_error ("Error line: "^l); ds) 213 ("Error while formating "^(command2string command)^" '"^id^"'!");
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_seq_monadScript.sml | 97 val _ = Hol_datatype `error_option = ValueState of 'a => 'b | Error of string`; 105 (errorT : string -> 'a M) e = K (Error e)`; 109 \y. case s y of Error e => Error e
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_seq_monadScript.sml | 97 val _ = Hol_datatype `error_option = ValueState of 'a => 'b | Error of string`; 105 (errorT : string -> 'a M) e = K (Error e)`; 110 \y. case s y of Error e => Error e
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | completion.scala | 77 case _: XML.Error => ignore_error(""); Nil 188 catch { case _: XML.Error => None }
|
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 119 val Error = """^(.*)---line (\d+) of file root.bib$""".r 132 case (Error(msg, Value.Int(l)), _) =>
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Map.sig | 39 val get : ('key,'a) map -> 'key -> 'a (* raises Error *)
|
H A D | Useful.sig | 13 exception Error of string exception
|
H A D | Tptp.sml | 573 | _ => raise Error "Tptp.destLiteral"; 857 | _ => raise Error "destCnfFormulaBody"; 864 | _ => raise Error "destFofFormulaBody"; 1755 | _ => raise Error "Tptp.destLineComment"; 1896 raise Error "TPTP problem has both cnf and fof conjecture formulas" 2081 | _ => raise Error "EOF inside a block comment"; 2115 handle Parse.NoParse => raise Error "parse error") 2116 handle Error err => 2117 raise Error ("error in TPTP file \"" ^ filename ^ "\" " ^ 2560 handle Error er [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | completion.scala | 77 case _: XML.Error => ignore_error(""); Nil 188 catch { case _: XML.Error => None }
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 119 val Error = """^(.*)---line (\d+) of file root.bib$""".r 132 case (Error(msg, Value.Int(l)), _) =>
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Map.sig | 39 val get : ('key,'a) map -> 'key -> 'a (* raises Error *)
|
H A D | Useful.sig | 13 exception Error of string exception
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_GraphBuildJ1.sml | 119 "] Error (ignored)");
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | traps.S | 61 /* The user context under SMP is always set to Error + 1 for the current 71 * FaultIP, and RSP) and are ready to push Error. 105 /* skip FaultIP, RSP, Error, NextIP, RFLAGS */ \ 487 /* skip RFLAGS, Error, NextIP, RSP, FaultIP */ 549 /* skip RFLAGS, NextIP, Error, RSP, FaultIP */ 595 pushq $-1 # set Error -1 to mean entry via syscall 638 push $-1 # set Error -1 to mean entry via syscall
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 39 case _: XML.Error => None 53 case _: XML.Error => None
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 39 case _: XML.Error => None 53 case _: XML.Error => None
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | TermParse.sml | 60 | Error (s,locn) => raise mk_HOL_ERRloc "Absyn" "Absyn" locn s 238 Error e => raise Preterm.mkExn e
|