/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | darwin.S | 39 #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 D | darwin_closure.S | 42 #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 D | type_strengthen.c | 192 int sg = 1; local 194 sg = -1; 201 x = 10 * x + sg * (*s - '0');
|
/seL4-l4v-10.1.1/HOL4/tools-poly/ |
H A D | build.sml | 63 | 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 D | selftest.sml | 193 [([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 D | tripleScript.sml | 108 \\ 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 D | summationScript.sml | 68 THEN sg `P (f (j:num):num) : bool`
|
H A D | binomialScript.sml | 117 THEN sg `(a * a EXP n
|
H A D | fermatScript.sml | 31 THEN sg `0 < n`
|
/seL4-l4v-10.1.1/HOL4/src/basicProof/ |
H A D | BasicProvers.sig | 54 val sg : term quotation -> tactic value
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Mutual.sml | 243 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 D | selftest.sml | 735 [([], 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 D | BuildCommand.sml | 84 | 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 D | cheney_allocScript.sml | 188 \\ 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 D | cheney_gcScript.sml | 452 \\ 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 D | bossLib.sml | 159 val sg = BasicProvers.sg value
|
H A D | bossLib.sig | 126 val sg : term quotation -> tactic value
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSLib.sml | 54 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 D | prog_x86Script.sml | 597 \\ 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 D | prog_ppcScript.sml | 106 \\ 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 D | prog_x64Script.sml | 702 \\ 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 D | prog_armScript.sml | 133 \\ 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 D | multiwordScript.sml | 249 \\ 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 D | lisp_initScript.sml | 20 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 D | YonedaScript.sml | 321 sg `TypedGraphFun (l,i) n ���> TypedGraphFun (i,j) h -:ens_cat (homs c)` >>
|