Searched refs:state (Results 1 - 25 of 512) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DlooprulesScript.sml262 ``!(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 Dpprint-file.lisp4 (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 Dfilter-forms.lisp6 (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 Dpprint-axioms.lisp6 (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 Dpkg-alist-to-alist.lisp17 (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 Da2ml.lisp12 (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 Duntranslate-file.lisp44 (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 Dbook-essence.lisp12 (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 Dcheck-file.lisp15 (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 DKripkeScript.sml13 * - 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 Ddebug.h89 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 DMMU_SetupScript.sml190 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 Dsynchronized.scala21 /* 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 Dsynchronized.scala21 /* 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 Dinterrupt.h115 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 DModelScript.sml11 (* - 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 DMachineTransitionScript.sml39 (* ``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 DhhWriter.sml73 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 Dlrtable.sml10 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 Dparser1.sml30 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 Dlrtable.sml10 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 Dparser1.sml30 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 DreachTools.sml22 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 DholCheck.sml16 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 Dffi.c404 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...]

Completed in 141 milliseconds

1234567891011>>