/seL4-l4v-master/isabelle/src/HOL/Mutabelle/lib/Tools/ |
H A D | mutabelle | 150 printf "%-40s C:$(count $1 "GenuineCex") P:$(count $1 "PotentialCex") N:$(count $1 "NoCex") T:$(count $1 "Timeout") D:$(count $1 "Donno") E: $(count $1 "Error")\n" "$1"
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sml | 52 if Name.equal x p then (a,b) else raise Error "Atom.destBinop: wrong binop" 53 | destBinop _ _ = raise Error "Atom.destBinop: not a binop"; 82 if h >= length tms then raise Error "Atom.subterm: bad path" 94 if h >= length tms then raise Error "Atom.replace: bad path" 148 raise Error "Atom.match" 164 raise Error "Atom.unify" 191 val _ = Term.equal l r orelse raise Error "Atom.destRefl" 201 val _ = not (Term.equal l r) orelse raise Error "Atom.sym: refl"
|
H A D | Subst.sml | 126 else raise Error "Subst.union: incompatible"; 140 if NameMap.inDomain w s then raise Error "Subst.invert: non-injective" 142 | inv (_, Term.Fn _, _) = raise Error "Subst.invert: non-variable"; 209 else raise Error "Subst.match: incompatible matches" 216 else raise Error "Subst.match: different structure" 217 | matchList _ _ = raise Error "Subst.match: functions can't match vars"; 234 else if Term.freeIn v tm then raise Error "Subst.unify: occurs check" 244 raise Error "Subst.unify: different structure";
|
H A D | Literal.sml | 61 | fromFormula _ = raise Error "Literal.fromFormula"; 117 val _ = pol1 = pol2 orelse raise Error "Literal.match" 128 val _ = pol1 = pol2 orelse raise Error "Literal.unify" 140 | destEq (false,_) = raise Error "Literal.destEq"; 147 | destNeq (true,_) = raise Error "Literal.destNeq"; 154 | destRefl (false,_) = raise Error "Literal.destRefl"; 160 fun destIrrefl (true,_) = raise Error "Literal.destIrrefl"
|
H A D | Clause.sml | 251 handle Error err => raise Error ("Clause.rewrite:\n" ^ err); 300 raise Error "resolve: clause1: ordering constraints" 305 raise Error "resolve: clause2: ordering constraints" 339 raise Error "Clause.paramodulate: with clause: ordering" 341 raise Error "Clause.paramodulate: into clause: ordering" 352 raise Error "Clause.paramodulate: equation: ordering constraints" 361 handle Error err => 365 raise Error err
|
H A D | Literal.sig | 99 val match : (* raises Error *) 106 val unify : (* raises Error *) 139 val sym : literal -> literal (* raises Error if given a refl or irrefl *)
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Mutabelle/lib/Tools/ |
H A D | mutabelle | 150 printf "%-40s C:$(count $1 "GenuineCex") P:$(count $1 "PotentialCex") N:$(count $1 "NoCex") T:$(count $1 "Timeout") D:$(count $1 "Donno") E: $(count $1 "Error")\n" "$1"
|
/seL4-l4v-master/seL4/include/arch/x86/arch/32/mode/machine/ |
H A D | registerset.h | 20 * double-word boundary, Error + 1 must be an even number of words 47 /* 0x24 */ Error = 9, enumerator in enum:_register
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTermnet.sml | 74 | SOME qtm' => if qtm = qtm' then sub else raise Error "matchq: vars"); 78 | qn _ ((Fn _, VAR) :: _) = raise Error "matchq: match fn var" 81 else raise Error "matchq: match fn fn"; 91 val () = assert (f = g) (Error "qunify: incompatible vars") 104 else raise Error "unifyq: structurally different"; 147 handle Error _ => raise Bug "mlibTermnet.insert: should never fail"; 170 handle Error _ => raise Bug "mlibTermnet.match: should never fail"; 227 handle Error _ => raise Bug "mlibTermnet.unify: should never fail"; 255 handle Error _ => raise Bug "mlibTermnet.matched: should never fail"; 279 handle Error [all...] |
H A D | mlibKernel.sml | 36 else raise Error "AXIOM: argument not a list of literals"; 42 else raise Error "ASSUME: argument not a literal";
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Literal.sml | 61 | fromFormula _ = raise Error "Literal.fromFormula"; 117 val _ = pol1 = pol2 orelse raise Error "Literal.match" 128 val _ = pol1 = pol2 orelse raise Error "Literal.unify" 140 | destEq (false,_) = raise Error "Literal.destEq"; 147 | destNeq (true,_) = raise Error "Literal.destNeq"; 154 | destRefl (false,_) = raise Error "Literal.destRefl"; 160 fun destIrrefl (true,_) = raise Error "Literal.destIrrefl"
|
H A D | Clause.sml | 251 handle Error err => raise Error ("Clause.rewrite:\n" ^ err); 300 raise Error "resolve: clause1: ordering constraints" 305 raise Error "resolve: clause2: ordering constraints" 339 raise Error "Clause.paramodulate: with clause: ordering" 341 raise Error "Clause.paramodulate: into clause: ordering" 352 raise Error "Clause.paramodulate: equation: ordering constraints" 361 handle Error err => 365 raise Error err
|
H A D | Literal.sig | 99 val match : (* raises Error *) 106 val unify : (* raises Error *) 139 val sym : literal -> literal (* raises Error if given a refl or irrefl *)
|
H A D | Rewrite.sml | 175 fun orderToOrient (SOME EQUAL) = raise Error "Rewrite.orient: reflexive" 246 val _ = id <> id' orelse raise Error "same theorem" 248 val _ = wellOriented ort lr orelse raise Error "orientation" 254 raise Error "order" 261 NONE => raise Error "Rewrite.rewrIdConv: no matching rewrites" 274 NONE => raise Error "incomparable" 280 if Term.equal tm r then (l,th) else raise Error "mkNeqConv: RL" 282 | SOME EQUAL => raise Error "irreflexive" 288 if Term.equal tm l then (r,th) else raise Error "mkNeqConv: LR" 351 handle Error er [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Useful.sml | 21 exception Error of string; exception 25 fun Error_to_string (Error message) = "\nError: " ^ message ^ "\n" 26 | Error_to_string _ = raise Bug "Error_to_string: not an Error exception"; 31 fun report (e as Error _) = Error_to_string e 33 | report _ = raise Bug "report: not an Error or Bug exception"; 38 handle h as Error _ => (print (Error_to_string h); raise h) 42 fun total f x = SOME (f x) handle Error _ => NONE; 46 fun partial (e as Error _) f x = (case f x of SOME y => y | NONE => raise e) 47 | partial _ _ _ = raise Bug "partial: must take an Error exception"; 241 | z _ _ _ = raise Error "zipwit [all...] |
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | AssembleHolindexParser.sml | 18 print ("Error: "^s^"\n");
|
/seL4-l4v-master/HOL4/tools/quote-filter/ |
H A D | mlton-quote-filter.sml | 39 (output(stdErr, "Error opening "^ifile^"\n");
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | AssembleHolfootParser.sml | 20 val _ = Parse.print_with_style [FG OrangeRed, Bold, Underline] "Error:";
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | c_traps.c | 179 if (likely(cur_thread->tcbArch.tcbContext.registers[Error] == -1) && 335 /* skip RFLAGS, Error, NextIP, RSP, and FaultIP */ 395 setRegister(NODE_STATE(ksCurThread), Error, irq_stack[0]); local
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/ |
H A D | determSemScript.sml | 54 | Error 82 | Error => Crash`; 102 (r = Error ��� ~sem_s.is_value r') ��� 174 (same_result sem_f sem_s Error s ���
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | channel.scala | 86 def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) } 90 def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | channel.scala | 86 def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) } 90 def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
|
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/machine/ |
H A D | registerset.h | 56 Error = 15, /* 0x78 */ enumerator in enum:_register
|
/seL4-l4v-master/seL4/src/arch/x86/32/ |
H A D | c_traps.c | 147 if (likely(NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[Error] == -1)) { 164 // skip FaultIP and Error (these are fake registers) 193 // skip FaultIP and Error
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Pretype.sml | 105 Error _ => Some (e, false) 129 | Error e => Error e (* should never happen *)) 143 | Error e => Error e 194 Error e => raise mkExn e
|