/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | protoparamshadow.c | 11 int var; variable 13 int proto(int var); 15 int realone(int var) argument 17 return var + 1; 22 var = var + 1; 23 return var; 26 int var = 4; variable
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Synchronized.sml | 9 type 'a var 10 val var: string -> 'a -> 'a var value 11 val value: 'a var -> 'a 12 val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option 13 val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b 14 val change_result: 'a var -> ('a -> 'b * 'a) -> 'b 15 val change: 'a var -> ('a -> 'a) -> unit 23 abstype 'a var = Var of 27 var 30 fun var name x = Var function [all...] |
H A D | Single_Assignment.sml | 9 type 'a var 10 val var: string -> 'a var value 11 val peek: 'a var -> 'a option 12 val await: 'a var -> 'a 13 val assign: 'a var -> 'a -> unit 19 abstype 'a var = Var of 23 var: 'a SingleAssignment.saref} 26 fun var name = Var function 30 var [all...] |
H A D | Thread_Data.sml | 9 type 'a var 10 val var: unit -> 'a var value 11 val get: 'a var -> 'a option 12 val put: 'a var -> 'a option -> unit 13 val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c 20 abstype 'a var = Var of 'a option Universal.tag 23 fun var () : 'a var = Var (Universal.tag ()); function
|
H A D | Counter.sml | 19 val counter = Synchronized.var "counter" 0;
|
/seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
H A D | quick.tex | 15 \newcommand{\var}[1]{{\emph{#1}}} 27 \hol{Theory}{new_theory} \var{name} & creates a new theory\\ 29 \hol{TotalDefn}{Define} \var{term} & function definition \\ 30 \hol{bossLib}{Hol_datatype} \var{type-dec} & defines a concrete datatype \\ 31 \holnoref{EquivType}{define_equivalence_type} \var{rec} & type of equivalence classes \\ 32 \hol{Theory}{save_thm}(\var{name},\var{thm}) & stores theorem \\ 33 \hol{Tactical}{prove}(\var{term},\var{tactic}) & proves theorem using tactic \\ 34 \hol{Tactical}{store_thm}(\var{nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | fdd.h | 87 inline bdd fdd_ithvarpp(int var, int val) argument 88 { return fdd_ithvar(var, val); } 90 inline bdd fdd_ithsetpp(int var) argument 91 { return fdd_ithset(var); } 93 inline bdd fdd_domainpp(int var) argument 94 { return fdd_domain(var); } 96 inline int fdd_scanvar(const bdd &r, int var) argument 97 { return fdd_scanvar(r.root, var); } 118 inline bdd* fdd_conpp(int bitnum, int var) 119 { return fdd_transfer( bitnum, fdd_con(bitnum, var) ); } [all...] |
H A D | fdd.c | 57 BDD var; /* The BDD variable set */ member in struct:s_Domain 178 domain[n+fdvarnum].var = bdd_makeset(domain[n+fdvarnum].ivar, 180 bdd_addref(domain[n+fdvarnum].var); 237 d->var = bdd_makeset(d->ivar, d->binsize); 238 bdd_addref(d->var); 287 PROTO {* int fdd_domainsize(int var) *} 289 block {\tt var}. *} 308 PROTO {* int fdd_varnum(int var) *} 310 block {\tt var}. *} 329 PROTO {* int *fdd_vars(int var) *} 377 fdd_ithvar(int var, int val) argument 429 fdd_scanvar(BDD r, int var) argument 522 fdd_ithset(int var) argument 551 fdd_domain(int var) argument 737 int *var; local 1057 fdddec2bin(int var, int val) argument [all...] |
H A D | bddop.c | 96 static int replacelast; /* Current last var. level to replace */ 147 #define RESTRHASH(r,var) (PAIR(r,var)) 310 PROTO {* BDD bdd_buildcube(int value, int width, BDD *var) 311 BDD bdd_ibuildcube(int value, int width, int *var)*} 313 var}. It does so by interpreting the {\tt width} low order 317 the first variables in {\tt var}. Consider as an example 318 the call {\tt bdd\_buildcube(0xB, 4, var)}. This corresponds 319 to the expression: $var[0] \conj \neg var[ 896 bdd_restrict(BDD r, BDD var) argument 1231 bdd_compose(BDD f, BDD g, int var) argument 1541 bdd_exist(BDD r, BDD var) argument 1592 bdd_forall(BDD r, BDD var) argument 1646 bdd_unique(BDD r, BDD var) argument 1745 bdd_appex(BDD l, BDD r, int opr, BDD var) argument 1811 bdd_appall(BDD l, BDD r, int opr, BDD var) argument 1877 bdd_appuni(BDD l, BDD r, int opr, BDD var) argument 2203 bdd_satoneset(BDD r, BDD var, BDD pol) argument 2229 satoneset_rec(BDD r, BDD var) argument [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.C | 94 if (proof != NULL) proof->resolve(unit_id[var(qs[i])], var(qs[i])); 107 unit_id[var(ps[0])] = (sign(ps[0])) ? -id : id; //HA: sign info 118 int max = level[var(ps[1])]; 120 if (level[var(ps[i])] > max) 121 max = level[var(ps[i])], 216 Var x = var(trail[c]); 251 bool operator () (Lit p, Lit q) { return trail_pos[var(p)] > trail_pos[var(q)]; } 276 if (!seen[var( [all...] |
H A D | SolverTypes.h | 44 explicit Lit(Var var, bool sgn = false) : x((var+var) + (int)sgn) {} argument 48 friend int var (Lit p); 61 inline int var (Lit p) { return p.x >> 1; } function 72 inline int toDimacs(Lit p) { return sign(p) ? -var(p) - 1 : var(p) + 1; }
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | selftest.sml | 72 (``rec "VM" (In "coin"..(In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") + 73 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))``, 78 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") + 79 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM"))) 92 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") + 93 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))) + 102 (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") + 103 In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))))���)];
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | problem-set-1-answers.lisp | 560 (defun boundp (var alist) 563 (if (equal var (car (car alist))) 565 (boundp var (cdr alist))))) 574 (defun binding (var alist) 577 (if (equal var (car (car alist))) 579 (binding var (cdr alist))))) 591 (defun bind (var val alist) 593 (cons (cons var (cons val nil)) nil) 594 (if (equal var (car (car alist))) 595 (cons (cons var (con [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 25 val peek : subst -> Term.var -> Term.term option 27 val insert : subst -> Term.var * Term.term -> subst 29 val singleton : Term.var * Term.term -> subst 31 val toList : subst -> (Term.var * Term.term) list 33 val fromList : (Term.var * Term.term) list -> subst 35 val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a 37 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
|
H A D | Formula.sig | 22 | Forall of Term.var * formula 23 | Exists of Term.var * formula 93 val destForall : formula -> Term.var * formula 97 val listMkForall : Term.var list * formula -> formula 101 val stripForall : formula -> Term.var list * formula 105 val destExists : formula -> Term.var * formula 109 val listMkExists : Term.var list * formula -> formula 113 val stripExists : formula -> Term.var list * formula 133 val freeIn : Term.var -> formula -> bool
|
H A D | Term.sig | 13 type var = Name.name type 22 Var of var 31 val destVar : term -> var 35 val equalVar : var -> term -> bool 107 val freeIn : var -> term -> bool 121 val variantPrime : NameSet.set -> var -> var 123 val variantNum : NameSet.set -> var -> var
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 25 val peek : subst -> Term.var -> Term.term option 27 val insert : subst -> Term.var * Term.term -> subst 29 val singleton : Term.var * Term.term -> subst 31 val toList : subst -> (Term.var * Term.term) list 33 val fromList : (Term.var * Term.term) list -> subst 35 val foldl : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a 37 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
|
H A D | Formula.sig | 22 | Forall of Term.var * formula 23 | Exists of Term.var * formula 93 val destForall : formula -> Term.var * formula 97 val listMkForall : Term.var list * formula -> formula 101 val stripForall : formula -> Term.var list * formula 105 val destExists : formula -> Term.var * formula 109 val listMkExists : Term.var list * formula -> formula 113 val stripExists : formula -> Term.var list * formula 133 val freeIn : Term.var -> formula -> bool
|
H A D | Term.sig | 13 type var = Name.name type 22 Var of var 31 val destVar : term -> var 35 val equalVar : var -> term -> bool 107 val freeIn : var -> term -> bool 121 val variantPrime : NameSet.set -> var -> var 123 val variantNum : NameSet.set -> var -> var
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfLibrary.sml | 53 val ((var, body), is_forall) = (boolSyntax.dest_forall t, true) value 58 (next_index + 1, (next_index, var, is_forall) :: vars, body) 93 (* 'CLAUSE_TO_SEQUENT'. Returns a list of triples ([~]i, [~]var, q), *) 138 val var = boolSyntax.dest_neg lit value 140 Thm.MP (Thm.INST [{redex = var, residue = boolSyntax.F}] 150 (* ----------------- bind_var hyp var true *) 151 (* A, !var. hyp |- t *) 154 (* ----------------- bind_var hyp var false (var not free in A or t) *) 155 (* A, ?var [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | liftScript.sml | 33 val vars = ty_antiq( ==`:var list`== ); 34 val subs = ty_antiq( ==`:(var # obj1) list`== ); 70 ``:(var # obj1) list``; 333 ���!s1:^subs s2 t1 t2 (t:var -> bool). 370 THEN IMP_RES_TAC (MATCH_MP FST_RSP (identity_quotient (==`:var`==))), 409 [ EXISTS_TAC ���x':var��� 414 EXISTS_TAC ���x':var��� 651 (* !(var : var->'a) obj inv upd cns nil par sgm. *) 656 (* (!x. ho (OVAR1 x) = var [all...] |
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | lnamelessScript.sml | 23 val _ = Datatype`lnt = var string | bnd num | app lnt lnt | abs lnt`; 27 (open k u (var s) = var s) /\ 34 (raw_lnpm pi (var s) = var (lswapstr pi s)) /\ 64 (fv (var s) = {s}) /\ 86 (!s. lclosed (var s)) /\ 88 (!s t. ~(s IN fv t) /\ lclosed (open 0 (var s) t) ==> 102 (!s c. P (var s) c) /\ 105 (!d. P (open 0 (var [all...] |
H A D | raw_syntaxScript.sml | 52 val _ = Hol_datatype `raw_term = var of string 57 (fv (var s) = {s}) /\ 68 (capt x (var y) = {}) /\ 87 (subst x y (var s) = if y = s then x else var s) /\ 95 ialpha y (lam x e) (lam y (subst (var y) x e))) /\ 113 ``!e x. subst (var x) x e = e``, 143 ``!e x y. ~(y IN fv e) ==> (subst (var x) y (subst (var y) x e) = e)``, 148 (collapse (var [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | liftScript.sml | 48 val subs = ty_antiq (``:(var # 'a term1) list``); 101 val ty = ``:(var # 'a term1) list``; 105 ``:(var # 'a term1) list``; 201 ���!s1:^subs s2 (t:var -> bool). 227 ���!s1:^subs s2 t1 t2 (t:var -> bool). 262 THEN IMP_RES_TAC (MATCH_MP FST_RSP (identity_quotient (==`:var`==))), 311 [ EXISTS_TAC ���x':var��� 316 EXISTS_TAC ���x':var��� 465 THEN EXISTS_TAC ���v:var��� 478 THEN EXISTS_TAC ���v:var��� [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
H A D | RecordType.sml | 208 val var = Psyntax.mk_var(app_letter typ, typ) value 310 val f = gen_var_domty("f", fupd, [var]) 312 Term`^(Term.inst s acc) (^fupd ^f ^var) = ^acc ^var` 317 val f = gen_var_domty("f", fupd, [var]) 319 Term`^(Term.inst s acc) (^fupd ^f ^var) = ^f (^acc ^var)` 322 val tactic = STRUCT_CASES_TAC (SPEC var cases_thm) THEN 374 val f = variant [var] (mk_var("f", fty)) 375 val g = variant [var, [all...] |