/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | looprulesScript.sml | 262 ``!(g :'a state -> bool) (body :'a command) (Inv :'a state -> bool) 266 (\(s :'a state). 269 (\(s :'a state). 272 (\(s :'a state). 274 (\(s :'a state). 275 (if L <= (Var :'a state -> int) s /\ Var s < H then 283 (\(s :'a state). 286 (\(s :'a state). 289 (\(s :'a state) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/obsolete/ |
H A D | pprint-file.lisp | 4 (set-state-ok t) 23 (defun pprint-file-fn (infile outfile ld-p state) 29 (er-let* ((forms (read-list infile ctx state)) 30 (axioms (expand-forms forms nil t nil ctx (w state) state))) 31 (write-list (reverse axioms) outfile ctx state))))) 36 `(pprint-file-fn ,infile ,outfile ,ld-p state))
|
H A D | filter-forms.lisp | 6 (set-state-ok t) 18 (defun expand-form (form untrans-flg state) 20 (let* ((wrld (w state)) 25 (er-let* ((tbody (translate body t t t 'top-level wrld state))) 58 (defun set-ld-redefinition-action-state (val state) 59 (mv-let (erp val state) 60 (set-ld-redefinition-action val state) 62 state)) 64 (defun expand-forms (forms acc untrans-flg logic-only ctx wrld state) [all...] |
H A D | pprint-axioms.lisp | 6 (set-state-ok t) 8 (defun pprint-axioms-fn (outfile state) 10 (getenv$ "ACL2_SYSTEM_BOOKS" state))) 22 outfile nil state)))) 28 :state-global-bindings 31 (set-raw-mode-on state) 33 (pprint-axioms-fn ,outfile state)))))
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/ |
H A D | pkg-alist-to-alist.lisp | 17 (set-state-ok t) 47 (defun print-string-triples-rec (triples chan state) 48 (declare (xargs :stobjs state 51 (open-output-channel-p chan :character state)))) 52 (cond ((endp triples) state) 58 chan state nil) 59 (print-string-triples-rec (cdr triples) chan state))))) 61 (defun print-objs-rec (objs chan state) 62 (declare (xargs :stobjs state 65 (open-output-channel-p chan :character state)))) [all...] |
H A D | a2ml.lisp | 12 (set-state-ok t) 57 (defun pprint-object (obj channel state) 58 (fms "~f0" (list (cons #\0 obj)) channel state nil)) 60 (defun pprint-objects-to-ml (list sep channel state) 63 state) 70 (pprint-objects-to-ml (cdr list) sep channel state)) 80 (pprogn (pprint-object (sexp-to-ml (car list)) channel state) 81 (newline channel state) 82 (if (endp (cdr list)) state (princ$ sep channel state)) [all...] |
H A D | untranslate-file.lisp | 44 (set-state-ok t) 102 (defun set-current-package-state (val state) 103 (mv-let (erp val state) 104 (set-current-package val state) 106 (cond (erp (prog2$ (er hard 'set-current-package-state 108 state)) 109 (t state)))) 111 (defun pprint-objects (lst ch state) 112 (cond ((null lst) state) [all...] |
H A D | book-essence.lisp | 12 (set-state-ok t) 14 (defun read-portcullis-cmds1 (chan cert-file ctx state acc) 15 (mv-let (eofp form state) 16 (read-object chan state) 30 (read-portcullis-cmds1 chan cert-file ctx state nil) 35 (read-portcullis-cmds1 chan cert-file ctx state acc)) 36 (t (read-portcullis-cmds1 chan cert-file ctx state 39 (defun read-portcullis-cmds (book-name cert-optional-p ctx state) 41 (extend-pathname (cbd) book-name state) 43 (mv-let (chan state) [all...] |
H A D | check-file.lisp | 15 (set-state-ok t) 44 (defun check-form (form ctx wrld state) 58 ctx wrld state))) 82 ctx wrld state))) 106 (defun check-form-lst (lst ignore-errors ctx wrld state) 109 (t (mv-let (erp val state) 110 (check-form (car lst) ctx wrld state) 113 (silent-error state)) 115 state))))))) 117 (defun check-file1 (infile ignore-errors state) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | KripkeScript.sml | 13 * - S : 'state is a set of states 14 * - S0 : 'state -> bool is a subset of S, the initial states 15 * - R : 'state # 'state -> bool is a transition relation 17 * - L : 'state -> ('prop -> bool) maps each state to the 18 * set of propositions true in that state 20 * N.B. terms that follow are not contrained to use type variables 'state and 70 * ``: ('state,'prop)kripke_structure`` 75 <| S: 'state [all...] |
/seL4-l4v-10.1.1/seL4/include/api/ |
H A D | debug.h | 89 char* state; local 92 state = "inactive"; 95 state = "running"; 98 state = "restart"; 101 state = "blocked on recv"; 104 state = "blocked on send"; 107 state = "blocked on reply"; 110 state = "blocked on ntfn"; 114 state = "running VM"; 118 state [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | MMU_SetupScript.sml | 190 val mmu_requirements_def = Define `mmu_requirements state id = 194 state.coprocessors.state.cp15.C1 195 state.coprocessors.state.cp15.C2 196 state.coprocessors.state.cp15.C3 198 state.memory) 204 /\ ((state.coprocessors.state [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Concurrent/ |
H A D | synchronized.scala | 21 /* state variable */ 23 private var state: A = init 25 def value: A = synchronized { state } 37 state = x1 43 val x = state 51 check(state) 70 def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() } 73 val (result, new_state) = f(state) 74 state [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Concurrent/ |
H A D | synchronized.scala | 21 /* state variable */ 23 private var state: A = init 25 def value: A = synchronized { state } 37 state = x1 43 val x = state 51 check(state) 70 def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() } 73 val (result, new_state) = f(state) 74 state [all...] |
/seL4-l4v-10.1.1/seL4/include/plat/pc99/plat/machine/ |
H A D | interrupt.h | 115 updateIRQState(irq_t irq, x86_irq_state_t state) argument 118 x86KSIRQState[irq] = state; 132 x86_irq_state_t state = x86KSIRQState[irq]; local 133 switch (x86_irq_state_get_irqType(state)) { 135 uint32_t ioapic = x86_irq_state_irq_ioapic_get_id(state); 136 uint32_t pin = x86_irq_state_irq_ioapic_get_pin(state); 138 state = x86_irq_state_irq_ioapic_set_masked(state, disable); 139 updateIRQState(irq, state);
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ModelScript.sml | 11 (* - S : 'state -> bool is a set of states *) 12 (* - S0 : 'state -> bool is a subset of S, the initial states *) 13 (* - R : 'state # 'state -> bool is a transition relation *) 15 (* - L : 'state -> ('prop -> bool) maps each state to the *) 16 (* set of propositions true in that state *) 18 (* The type parameters are: ``: ('state,'prop)model`` *) 19 (* N.B. terms that follow are not contrained to use type variables 'state *) 60 (* ``: ('prop,'state)mode [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | MachineTransitionScript.sml | 39 (* ``Next R B state'' is true if state can be reached from *) 40 (* a state satisfying B in one R-step *) 45 `Next R B state = 46 ?state_. B state_ /\ R(state_,state)`; 49 (* ``Prev R Q state'' is the set of states from which Q can be reached *) 55 `Prev R Q state = ?state'. R(state,state') /\ [all...] |
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhWriter.sml | 73 fun store_name state name = 74 let val dict = #used_names state in 79 fun declare_perm_type state {Thy,Name} = 83 val dict = #ty_names state 85 store_name state name1; (* may be deprecated *) 91 fun declare_perm_const state {Thy,Name} = 95 val dict = #const_names state 97 store_name state name1; 103 fun declare_perm_thm state (thy,n) name = 107 val dict = #thm_names state 384 val state = value 432 val state = value [all...] |
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | lrtable.sml | 10 datatype state = STATE of int type 11 datatype action = SHIFT of state 15 exception Goto of state * nonterm 16 type table = {states: int, rules : int,initialState: state, 18 goto : (nonterm,state) pairlist array} 44 fn (STATE state,term) => 45 let val (row,default) = action sub state 49 fn (a as (STATE state,nonterm)) => 50 case findNonterm(nonterm,goto sub state) 51 of SOME state [all...] |
H A D | parser1.sml | 30 type ('a,'b) elem = (state * ('a * 'b * 'b)) 37 of (state, _) :: rest => 39 println(showState state); 54 let fun prAction(stack as (state, _) :: _, 56 (println "Parse: state stack:"; 58 print(" state=" 59 ^ showState state 77 stack as (state,_) :: _ : ('_b ,'_c) stack) = 78 case (if DEBUG then prAction(stack, next,action(state, terminal)) 79 else action(state, termina [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | lrtable.sml | 10 datatype state = STATE of int type 11 datatype action = SHIFT of state 15 exception Goto of state * nonterm 16 type table = {states: int, rules : int,initialState: state, 18 goto : (nonterm,state) pairlist array} 44 fn (STATE state,term) => 45 let val (row,default) = action sub state 49 fn (a as (STATE state,nonterm)) => 50 case findNonterm(nonterm,goto sub state) 51 of SOME state [all...] |
H A D | parser1.sml | 30 type ('a,'b) elem = (state * ('a * 'b * 'b)) 37 of (state, _) :: rest => 39 println(showState state); 54 let fun prAction(stack as (state, _) :: _, 56 (println "Parse: state stack:"; 58 print(" state=" 59 ^ showState state 77 stack as (state,_) :: _ : ('_b ,'_c) stack) = 78 case (if DEBUG then prAction(stack, next,action(state, terminal)) 79 else action(state, termina [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | reachTools.sml | 22 fun RiterComputeReachable tbR tbS s sp2s n state state' Rname Iname etqcth = 24 val rcth = ISPECL [Rname,Iname,n,state] reachTheory.ReachableRecSimp 25 val rcth' = PURE_ONCE_REWRITE_RULE [GEN_PALPHA_CONV state' (snd(dest_disj(rhs(concl rcth))))] rcth 30 then let val eqth = PairRules.PGEN state (BddThmOracle (BddOp(bdd.Biimp,tbS,tbS2'))) 32 val eqth2 = REWRITE_RULE [REWRITE_RULE [GEN_PALPHA_CONV state (lhs (concl feqth))] feqth] eqth 33 in BddEqMp (AP_THM (SYM (MATCH_MP (ISPECL [Rname,Iname,n] reachTheory.ReachableFP) eqth2)) state) tbS end 34 else RiterComputeReachable tbR tbS2' s sp2s ``SUC ^n`` state state' Rname Iname etqcth end; 37 let val state value [all...] |
H A D | holCheck.sml | 16 val (I1,T1,Ric,ksname,bvm,state,fl,_,ic) = dest_model model 17 val state = if isSome state then valOf state else mk_state I1 T1 value 18 val (apl,apsubs) = if get_flag_abs model then holCheckTools.mk_abs_APs fl state else (NONE,[]) 19 val vm = mk_varmap state bvm 21 in (I1,T1,Ric,ksname,bvm,state,fl,ic,vm,apl,apsubs) end 28 val (I1,T1,Ric,ksname,bvm,state,fl,ic,vm,apl,apsubs) = init model 36 then let val (r,(i,c)) = absCheck I1 T1 state Ric vm ksname (get_abs ic,get_common ic) 39 else let val (r,(i,c)) = ctlCheck I1 T1 state Ri [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/aarch64/ |
H A D | ffi.c | 404 state. 406 The terse state variable names match the names used in the AARCH64 420 /* Initialize a procedure call argument marshalling state. */ 422 arg_init (struct arg_state *state, size_t call_frame_size) argument 424 state->ngrn = 0; 425 state->nsrn = 0; 426 state->nsaa = 0; 429 state->allocating_variadic = 0; 437 available_x (struct arg_state *state) argument 439 return N_X_ARG_REG - state 446 available_v(struct arg_state *state) argument 452 allocate_to_x(struct call_context *context, struct arg_state *state) argument 459 allocate_to_s(struct call_context *context, struct arg_state *state) argument 466 allocate_to_d(struct call_context *context, struct arg_state *state) argument 473 allocate_to_v(struct call_context *context, struct arg_state *state) argument 481 allocate_to_stack(struct arg_state *state, void *stack, size_t alignment, size_t size) argument 556 copy_hfa_to_reg_or_stack(void *memory, ffi_type *ty, struct call_context *context, unsigned char *stack, struct arg_state *state) argument 591 allocate_to_register_or_stack(struct call_context *context, unsigned char *stack, struct arg_state *state, unsigned short type) argument 642 copy_to_register_or_stack(struct call_context *context, unsigned char *stack, struct arg_state *state, void *value, unsigned short type) argument 662 struct arg_state state; local 971 struct arg_state state; local [all...] |