/seL4-l4v-master/HOL4/developers/ |
H A D | mosmlsysinfo.sml | 2 (List.nth([], 1) handle Option => "2.01" | Subscript => "2.10")^
|
H A D | polysysinfo.sml | 4 handle Empty => "" 7 handle Option => 0
|
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | posix_interrupt.scala | 18 val new_handler = new SignalHandler { def handle(s: Signal) { h } } 19 val old_handler = Signal.handle(SIGINT, new_handler) 20 try { e } finally { Signal.handle(SIGINT, old_handler) }
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | posix_interrupt.scala | 18 val new_handler = new SignalHandler { def handle(s: Signal) { h } } 19 val old_handler = Signal.handle(SIGINT, new_handler) 20 try { e } finally { Signal.handle(SIGINT, old_handler) }
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patriciaSyntax.sml | 46 handle HOL_ERR _ => raise ERR "mk_empty" ""; 50 handle HOL_ERR _ => raise ERR "mk_leaf" ""; 54 handle HOL_ERR _ => raise ERR "mk_branch" ""; 58 handle HOL_ERR _ => raise ERR "mk_peek" ""; 62 handle HOL_ERR _ => raise ERR "mk_find" ""; 66 handle HOL_ERR _ => raise ERR "mk_add" ""; 70 handle HOL_ERR _ => raise ERR "mk_add_list" ""; 74 handle HOL_ERR _ => raise ERR "mk_remove" ""; 78 handle HOL_ERR _ => raise ERR "mk_traverse" ""; 82 handle HOL_ER [all...] |
H A D | patricia_castsSyntax.sml | 70 handle HOL_ERR _ => raise ERR "mk_wordempty" ""; 75 end handle HOL_ERR _ => raise ERR "mk_the_ptree" ""; 80 handle HOL_ERR _ => raise ERR "mk_some_ptree" ""; 85 end handle HOL_ERR _ => raise ERR "mk_peekw" ""; 90 end handle HOL_ERR _ => raise ERR "mk_findw" ""; 95 end handle HOL_ERR _ => raise ERR "mk_addw" ""; 100 end handle HOL_ERR _ => raise ERR "mk_add_listw" ""; 105 end handle HOL_ERR _ => raise ERR "mk_removew" ""; 110 end handle HOL_ERR _ => raise ERR "mk_traversew" ""; 115 end handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | SGAUnicodeMergeBScript.sml | 14 REWRITE_TAC[]) handle HOL_ERR _ => (numfails := 1; TRUTH) 19 REWRITE_TAC[]) handle HOL_ERR _ => (numfails := !numfails + 1; TRUTH)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | temporal_stateSyntax.sml | 18 progSyntax.dest_spec tm handle HOL_ERR _ => dest_temporal_next tm 19 fun dest_pre' tm = progSyntax.dest_pre tm handle HOL_ERR _ => dest_pre tm 20 fun dest_code' tm = progSyntax.dest_code tm handle HOL_ERR _ => dest_code tm 21 fun dest_post' tm = progSyntax.dest_post tm handle HOL_ERR _ => dest_post tm 23 progSyntax.dest_pre_post tm handle HOL_ERR _ => dest_pre_post tm
|
/seL4-l4v-master/HOL4/tools/cmp/ |
H A D | cmp.sml | 10 BinIO.openIn s handle IO.Io _ => die ("Bad file: "^s) 21 handle IO.Io _ => die "File 1 had I/O error" 23 handle IO.Io _ => die "File 2 had I/O error"
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | holmakebuild.sml | 11 handle (e as HOL_ERR _) =>
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | github196Script.sml | 9 handle HOL_ERR _ => print "Test-case OK\n"
|
/seL4-l4v-master/HOL4/src/opentheory/logging/ |
H A D | skico.sml | 7 handle Feedback.HOL_ERR e => (print (Feedback.format_ERR e); raise D)
|
/seL4-l4v-master/HOL4/src/opentheory/postbool/ |
H A D | holdecide.sml | 7 handle Feedback.HOL_ERR e => (print (Feedback.format_ERR e); raise D)
|
/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | Exn.sml | 12 fun capture f x = Res (f x) handle e => Exn e
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | mosml_Holmake.sml | 8 handle Interrupt => die_with "Holmake interrupted"
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Mosml.sml | 34 handle IO.Io _ => Failure (cmd ^ ": command failed")) 36 (OS.FileSys.remove infile) handle OS.SysErr _ => (); 37 (OS.FileSys.remove outfile) handle OS.SysErr _ => (); 40 handle e => 41 ((OS.FileSys.remove infile) handle OS.SysErr _ => (); 42 (OS.FileSys.remove outfile) handle OS.SysErr _ => ();
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_astSyntax.sml | 186 handle HOL_ERR _ => raise ERR "mk_Mode1_immediate" ""; 190 handle HOL_ERR _ => raise ERR "mk_Mode1_register" ""; 195 handle HOL_ERR _ => raise ERR "mk_Mode1_register_shifted_register" ""; 199 handle HOL_ERR _ => raise ERR "mk_Mode2_immediate" ""; 203 handle HOL_ERR _ => raise ERR "mk_Mode2_register" ""; 207 handle HOL_ERR _ => raise ERR "mk_Mode3_immediate" ""; 211 handle HOL_ERR _ => raise ERR "mk_Mode3_register" ""; 215 handle HOL_ERR _ => raise ERR "mk_Hint_debug" ""; 221 handle HOL_ERR _ => raise ERR "mk_Branch" ""; 225 handle HOL_ER [all...] |
H A D | armSyntax.sml | 27 end handle HOL_ERR _ => raise err 94 handle HOL_ERR _ => raise ERR "mk_error" ""; 100 handle HOL_ERR _ => raise ERR "mk_valuestate" ""; 104 handle HOL_ERR _ => raise ERR "mk_constT" ""; 111 handle HOL_ERR _ => raise ERR "mk_seqT" ""; 117 handle HOL_ERR _ => raise ERR "mk_parT" ""; 123 handle HOL_ERR _ => raise ERR "mk_forT" ""; 128 handle HOL_ERR _ => raise ERR "mk_readT" ""; 132 handle HOL_ERR _ => raise ERR "mk_writeT" ""; 138 handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_astSyntax.sml | 186 handle HOL_ERR _ => raise ERR "mk_Mode1_immediate" ""; 190 handle HOL_ERR _ => raise ERR "mk_Mode1_register" ""; 195 handle HOL_ERR _ => raise ERR "mk_Mode1_register_shifted_register" ""; 199 handle HOL_ERR _ => raise ERR "mk_Mode2_immediate" ""; 203 handle HOL_ERR _ => raise ERR "mk_Mode2_register" ""; 207 handle HOL_ERR _ => raise ERR "mk_Mode3_immediate" ""; 211 handle HOL_ERR _ => raise ERR "mk_Mode3_register" ""; 215 handle HOL_ERR _ => raise ERR "mk_Hint_debug" ""; 221 handle HOL_ERR _ => raise ERR "mk_Branch" ""; 225 handle HOL_ER [all...] |
H A D | armSyntax.sml | 27 end handle HOL_ERR _ => raise err 95 handle HOL_ERR _ => raise ERR "mk_error" ""; 101 handle HOL_ERR _ => raise ERR "mk_valuestate" ""; 105 handle HOL_ERR _ => raise ERR "mk_constT" ""; 112 handle HOL_ERR _ => raise ERR "mk_seqT" ""; 118 handle HOL_ERR _ => raise ERR "mk_parT" ""; 124 handle HOL_ERR _ => raise ERR "mk_forT" ""; 129 handle HOL_ERR _ => raise ERR "mk_readT" ""; 133 handle HOL_ERR _ => raise ERR "mk_writeT" ""; 139 handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | codegen_inputLib.sml | 81 fun dest_x tm = ASSIGN_X_REG (dest_reg tm) handle e => ASSIGN_X_CONST (dest_n2w tm) 82 fun dest_address tm = ASSIGN_ADDRESS_REG (dest_reg tm) handle e => 84 ASSIGN_ADDRESS_OFFSET_ADD ((dest_reg o cdr o car) tm, dest_n2w (cdr tm))) handle e => 102 handle e => let 103 val (i,_) = match_term ``(f:word32->word8) a = n2w n`` tm handle e => 108 handle e => 116 val tm = ((snd o dest_eq o concl o c) tm) handle e => tm 153 in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let 159 in (ACCESS_BYTE,addr,x) end handle HOL_ERR _ => let 164 in (ACCESS_BYTE,addr,ASSIGN_X_CONST x) end handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegen_inputLib.sml | 77 fun dest_x tm = ASSIGN_X_REG (dest_reg tm) handle e => ASSIGN_X_CONST (dest_n2w tm) 78 fun dest_address tm = ASSIGN_ADDRESS_REG (dest_reg tm) handle e => 80 ASSIGN_ADDRESS_OFFSET_ADD ((dest_reg o cdr o car) tm, dest_n2w (cdr tm))) handle e => 98 handle e => let 99 val (i,_) = match_term ``(f:word64->word8) a = n2w n`` tm handle e => 104 handle e => 112 val tm = ((snd o dest_eq o concl o c) tm) handle e => tm 131 in (ACCESS_WORD,addr) end handle HOL_ERR _ => fail() 135 in (ACCESS_BYTE,addr) end handle HOL_ERR _ => fail() 151 in (ACCESS_WORD,addr,x) end handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/tools/ |
H A D | unquote-init.sml | 21 end handle Io _ => false 34 handle e => (FileSys.remove filename handle _ => (); raise e)
|
/seL4-l4v-master/HOL4/src/refute/ |
H A D | Canon.sml | 78 handle e as (HOL_ERR _) => WRAP_ERR("ONEWAY_SKOLEM_CONV",e)) 195 handle HOL_ERR _ => 212 handle HOL_ERR _ => 220 handle HOL_ERR _ => NNF_CONV_TERMINAL emb bvs tm 223 handle HOL_ERR _ => NNF_CONV_TERMINAL emb bvs tm 235 handle HOL_ERR _ => 253 handle HOL_ERR _ => 260 end handle HOL_ERR _ 264 handle HOL_ERR _ => NNF_CONV_TERMINAL emb bvs (mk_neg tm) 275 handle HOL_ER [all...] |
/seL4-l4v-master/HOL4/src/pfl/ |
H A D | pflLib.sml | 35 handle e => raise ERR "DLEM_TAC" "unable to prove stability lemma"; 53 handle e => raise ERR "is_some_ifn_thm" "tactic failed" 63 handle e => raise ERR "is_ifn_some_thm" "tactic failed" 70 handle e => raise ERR "ifn_dlem" "tactic failed" 82 handle e => raise ERR "ifn_mono_thm" "tactic failed" 96 handle e => raise ERR "ifn_norm_thm" "tactic failed" 105 handle e => raise ERR "ifn_determ_thm" "tactic failed" 110 handle e => raise wrap_exn "basic_lemmas" "proof failed" e;
|