Searched refs:Abort (Results 1 - 13 of 13) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
| H A D | syntaxScript.sml | 69 Abort
101 `(guards cs [] = if cs = [] then Abort else Nondets cs) /\
109 `(Probs [] = Abort) /\
|
| H A D | relScript.sml | 130 `(rel Abort = \s m. m IN Measure) /\
|
| H A D | wpScript.sml | 53 `(wp Abort = \r. Zero) /\
85 (``healthy (wp Abort)``,
91 val () = print "wp Abort is healthy\n";
951 (* Anything refines Abort *)
956 ``!p. refines (wp Abort) (wp p)``,
1011 `(wlp Abort = \r. Magic) /\
1021 (* [It's obvious that wlp can't be healthy, because wlp Abort Zero = Magic.] *)
1104 ``!post. Leq Magic (wlp Abort post)``,
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | convert_loop_bounds.py | 69 except problem.Abort, e:
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | problem.py | 18 class Abort(Exception): class in inherits:Exception
87 raise Abort ()
517 raise Abort ()
787 raise Abort ()
|
| H A D | graph-refine.py | 92 except problem.Abort:
|
| H A D | loop_bounds.py | 684 except problem.Abort, e:
897 except problem.Abort, e:
|
| H A D | trace_refute.py | 615 except problem.Abort:
|
| H A D | stack_logic.py | 645 except problem.Abort, e:
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_seq_monadScript.sml | 257 | 0b10111w => read__psr ii SPSR_abt (* Abort mode *)
275 | 0b10111w => write__psr ii SPSR_abt value (* Abort mode *)
357 | 0b10111w => abt (* Abort mode *)
|
| H A D | arm_stepLib.sml | 1030 ["Abt", "Abort"],
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
| H A D | arm_seq_monadScript.sml | 263 | 0b10111w => read__psr ii SPSR_abt (* Abort mode *)
281 | 0b10111w => write__psr ii SPSR_abt value (* Abort mode *)
363 | 0b10111w => abt (* Abort mode *)
|
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | PairedLambda.sml | 302 (*check which variables are used / unused. Abort if
|
Completed in 115 milliseconds