Searched refs:sg (Results 1 - 25 of 69) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Ddarwin.S39 #define sg MODE_CHOICE(stw,std) define
94 sg r9,(LINKAGE_SIZE+6*GPR_BYTES)(r8)
101 sg r9,SAVED_LR_OFFSET(r8)
103 sg r28,-(4 * GPR_BYTES)(r8)
104 sg r29,-(3 * GPR_BYTES)(r8)
105 sg r30,-(2 * GPR_BYTES)(r8)
106 sg r31,-( GPR_BYTES)(r8)
110 sg r2,(5 * GPR_BYTES)(r1)
199 sg r3, (LINKAGE_SIZE )(r28)
200 sg r
[all...]
H A Ddarwin_closure.S42 #define sg MODE_CHOICE(stw,std) define
138 sg r0,SAVED_LR_OFFSET(r1) /* save the return address */
149 sg r3, (PARENT_PARM_BASE )(r1)
150 sg r4, (PARENT_PARM_BASE + GPR_BYTES )(r1)
151 sg r5, (PARENT_PARM_BASE + GPR_BYTES * 2)(r1)
152 sg r6, (PARENT_PARM_BASE + GPR_BYTES * 3)(r1)
153 sg r7, (PARENT_PARM_BASE + GPR_BYTES * 4)(r1)
154 sg r8, (PARENT_PARM_BASE + GPR_BYTES * 5)(r1)
155 sg r9, (PARENT_PARM_BASE + GPR_BYTES * 6)(r1)
156 sg r1
[all...]
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dtype_strengthen.c192 int sg = 1; local
194 sg = -1;
201 x = 10 * x + sg * (*s - '0');
/seL4-l4v-10.1.1/HOL4/tools-poly/
H A Dbuild.sml63 | W_SIGNALED sg => "with signal " ^
64 SysWord.toString (Posix.Signal.toWord sg)
65 | W_STOPPED sg => "stopped with signal " ^
66 SysWord.toString (Posix.Signal.toWord sg)
/seL4-l4v-10.1.1/HOL4/src/q/
H A Dselftest.sml193 [([abb], sg)] =>
195 Term.aconv sg ``v ==> y < z``
216 [([abb], sg)] =>
218 Term.aconv sg ``(!y. y < SUC zero) /\ v``
227 [([abb], sg)] =>
229 Term.aconv sg ``(!y. y < SUC zero) /\ v``
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DtripleScript.sml108 \\ REVERSE (sg `q' /\ (?n. ~g (FUNPOW f n x)) = q'`)
126 \\ REVERSE (sg `q' /\ (?n. ~g (FUNPOW f n x)) = q'`)
/seL4-l4v-10.1.1/HOL4/examples/RSA/
H A DsummationScript.sml68 THEN sg `P (f (j:num):num) : bool`
H A DbinomialScript.sml117 THEN sg `(a * a EXP n
H A DfermatScript.sml31 THEN sg `0 < n`
/seL4-l4v-10.1.1/HOL4/src/basicProof/
H A DBasicProvers.sig54 val sg : term quotation -> tactic value
/seL4-l4v-10.1.1/HOL4/src/1/
H A DMutual.sml243 let val (sg,pf) = t (A,tm) in ([sg],[pf]) end value
247 val (sg,pf) = h (A,conj1) value
249 ((sg::sgs),(pf::pfs))
H A Dselftest.sml735 [([], sg)] => let val (sg1,sg2) = dest_conj sg
751 [([], sg)] => if aconv sg expected then OK() else die ""
766 [([], sg)] => if aconv sg ``^P (b:'a)`` then OK()
779 [([], sg)] => if aconv sg ``?x:'a. PP x (a:'a)`` then OK()
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/
H A DBuildCommand.sml84 | W_SIGNALED sg => "with signal " ^
85 SysWord.toString (Posix.Signal.toWord sg)
86 | W_STOPPED sg => "stopped with signal " ^
87 SysWord.toString (Posix.Signal.toWord sg)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Dcheney_allocScript.sml188 \\ sg `!x. b (g x) = x` \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,IN_DEF]);
250 \\ REPEAT STRIP_TAC \\ sg `basic_abs m = {}` \\ ASM_REWRITE_TAC [CARD_EMPTY]
254 REPEAT STRIP_TAC \\ sg `ok_state_part (i,i+j,(i+j =+ EMP) m)` THENL [
266 \\ sg `(basic_abs m = (i+j,x,y,d) INSERT xxx) /\ ~((i+j,x,y,d) IN xxx)`
282 \\ sg `basic_abs m = {}` \\ ASM_SIMP_TAC bool_ss [CARD_EMPTY]
315 sg `ch_set (FEMPTY:num|->num#num#'a) = {}`
319 sg `ch_set ((f |+ (x,y)):num|->num#num#'a) = (x,y) INSERT ch_set f`
840 \\ sg `reachables (x::xs) (ch_set h) = reachables xs (ch_set h)`
862 \\ sg `reachables (x2::x1::xs) (ch_set h) = reachables xs (ch_set h)`
932 sg `ch_se
[all...]
H A Dcheney_gcScript.sml452 \\ sg `!xx. R1 ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) xx = (j = xx) \/ R1 m xx`
587 \\ sg `RANGE (j,j2) x' \/ RANGE (i,j) x'` THENL [
681 (sg `D0 (CUT (b,j'') ((i =+ DATA (x',y',d)) m'')) =
695 \\ sg `D1 (CUT (i,i + 1) ((i =+ DATA (x',y',d))m'')) = {x';y'}` THENL [
725 (sg `RANGE (b,j) i /\ RANGE (b,j') i`
768 \\ sg `abs ((i =+ DATA (x',y',d))m'') = abs m''` THENL [
822 \\ sg `(RANGE (i,i + SUC j) = (i + j) INSERT RANGE (i,i + j)) /\
831 \\ sg `RANGE (i,j) = EMPTY` \\ ASM_REWRITE_TAC [FINITE_EMPTY,CARD_EMPTY]
845 \\ sg `!k. RANGE(b,i)k ==> IRANGE (b2,b2 + l) k`
1203 \\ sg `ab
[all...]
/seL4-l4v-10.1.1/HOL4/src/boss/
H A DbossLib.sml159 val sg = BasicProvers.sg value
H A DbossLib.sig126 val sg : term quotation -> tactic value
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSLib.sml54 let val res as (sg, _) = tac g
55 val _ = print ("subgoals: " ^ Int.toString (List.length sg) ^ "\n")
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dprog_x86Script.sml597 \\ sg `~(xMem a (SOME (w,xDATA_PERM e)) b IN xBYTE_MEMORY_ANY_SET (df DELETE a) g e c)`
677 \\ sg `!f. xBYTE_MEMORY_ANY F {} (xMEMORY_FUNC f) = emp`
858 \\ Induct \\ sg `{n2w n | n < 0} = {}`
860 \\ sg `{n2w n | n < SUC k} = n2w k INSERT {n2w n | n < k}`
972 \\ sg `CODE_POOL X86_INSTR ((a + 0x1w,xs,T) INSERT (a,[x],T) INSERT s) =
989 \\ sg `{(a + n2w n,[EL n (h::xs)],T) | n | n < LENGTH (h::xs)} =
1006 \\ sg `CODE_POOL X86_INSTR ((a,[],T) INSERT s) =
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dprog_ppcScript.sml106 \\ sg `~((?x. pReg a x IN ppc2set'' y s) = (?x. pReg a x IN ppc2set'' y' s'))`,
108 \\ sg `~((?x. pMem a x IN ppc2set'' y s) = (?x. pMem a x IN ppc2set'' y' s'))`,
110 \\ sg `~((?x. pStatus a x IN ppc2set'' y s) = (?x. pStatus a x IN ppc2set'' y' s'))`]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dprog_x64Script.sml702 \\ sg `~(zMem a (SOME (w,zDATA_PERM e)) b IN zBYTE_MEMORY_ANY_SET (df DELETE a) g e c)`
854 \\ REVERSE (sg `zMEMORY {} f = emp`)
1020 \\ REVERSE (sg `zMEMORY64 {} f = emp`)
1240 \\ sg `CODE_POOL X64_INSTR ((a + 0x1w,xs) INSERT (a,[x]) INSERT s) =
1257 \\ sg `{(a + n2w n,[EL n (h::xs)]) | n | n < LENGTH (h::xs)} =
1274 \\ sg `CODE_POOL X64_INSTR ((a,[]) INSERT s) =
1306 \\ REVERSE (sg `CODE_POOL X64_INSTR
1317 \\ REVERSE (sg `CODE_POOL X64_INSTR
1467 \\ sg `{(a + n2w n,[EL n xs]) | n | n < LENGTH xs} = {(a,[f a]) | a IN df}`
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armScript.sml133 \\ sg `~((?x. aReg a x IN arm2set'' y s) = (?x. aReg a x IN arm2set'' y' s'))`,
135 \\ sg `~((?x. aMem a x IN arm2set'' y s) = (?x. aMem a x IN arm2set'' y' s'))`,
137 \\ sg `~((?x. aStatus a x IN arm2set'' y s) = (?x. aStatus a x IN arm2set'' y' s'))`,
138 sg `~((?x. aCPSR_Reg x IN arm2set'' y s) = (?x. aCPSR_Reg x IN arm2set'' y' s'))`,
139 sg `~((?x. aUndef x IN arm2set'' y s) = (?x. aUndef x IN arm2set'' y' s'))`]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/multiword/
H A DmultiwordScript.sml249 \\ REV (sg `~(n2mw (n DIV dimword (:'a)) = ([]:'a word list))`)
341 \\ REV (sg `m DIV dimword (:'a) <= n DIV dimword (:'a)`) THEN1 METIS_TAC []
491 \\ REV (sg `(n + n' + b2n c) DIV dimword (:'a) = 1`)
1024 (REV (sg `mw2n (SNOC x xs) < mw2n (SNOC z zs)`) THEN1 DECIDE_TAC
2177 REV (sg `mw_cmp [u3; u2; u1] (mw_mul_by_single q [v2; v1]) = SOME T`)
2187 REV (sg `w2n u1 * dimword(:'a) * dimword(:'a) + w2n u2 * dimword(:'a) + w2n u3 < w2n q * (w2n v1 * dimword(:'a) + w2n v2)`)
2384 sg `w2n q3 = mw2n (REVERSE us) DIV mw2n (REVERSE ys)`
2515 sg `w2n q3 = mw2n (REVERSE us) DIV mw2n (REVERSE ys)`
2814 (sg `mw_mul_by_single d (mw_fix ys) <> []`
3436 \\ sg `w2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_initScript.sml20 fun SUBGOAL q = REVERSE (sg q)
95 \\ sg `dg DIFF (a INSERT xs) = dg DIFF xs DELETE a`
/seL4-l4v-10.1.1/HOL4/examples/category/
H A DYonedaScript.sml321 sg `TypedGraphFun (l,i) n ���> TypedGraphFun (i,j) h -:ens_cat (homs c)` >>

Completed in 274 milliseconds

123