/seL4-l4v-master/l4v/tools/c-parser/testfiles/errors/ |
H A D | addrlocal.c | 7 void swap(int *i1, int *i2) argument 11 *i1 = *i2; 12 *i2 = tmp;
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | mux.ml | 4 (`NAND_SPEC`, "!i1 i2 o. NAND_SPEC(i1,i2,o) = o = ~(i1 /\ i2)");; 10 (`MUX_SPEC`, "!c i1 i2 o. MUX_SPEC(c,i1,i2,o) = o = (c => i1 | i2)");; 14 "!c i1 i2 o. 15 MUX_IMP(c,i1,i2,o) = 18 NAND_SPEC(l1,i2,l2) /\
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/MISC/ |
H A D | myfun.ml | 8 |- !i1 i2 m n t. 9 MULT_FUN((i1,i2),m,n,t) = 12 MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0)))) 20 "!i1 i2 m n. 21 MULT_FUN((i1,i2),m,n,T) = (m,n,T)", 29 "!i1 i2 m n. 30 MULT_FUN((i1,i2),m,n,F) = 31 MULT_FUN((i1,i2),((i [all...] |
H A D | mk_COUNT.ml | 23 "MUX(switch,i1:^sig,i2:^sig,o:^sig) = (o = (switch -> i1 | i2))");;
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | gates.ml | 19 let nand = new_definition (`nand`,"nand (i1,i2) = ~(i1 /\ i2)");; 20 let and = new_definition (`and`,"and (i1,i2) = (i1 /\ i2)");; 21 let xor = new_definition (`xor`,"xor (i1,i2) = (i1 /\ ~i2) \/ (~i1 /\ i2)");; 35 "NAND_IMP (i1:^wire,i2:^wire,o:^wire) = 39 Ptran (i2,w1,w3) /\ 43 Ntran (i2,w [all...] |
H A D | muxn.ml | 18 let mux = new_definition (`mux`,"mux (cntl,i1:*,i2:*) = cntl => i1 | i2");; 22 "CMUX_IMP (cntl:^wire,cntlbar:^wire,i1:^wire,i2:^wire,o:^wire) = 29 Ptran (cntl,i2,w5) /\ 30 Ntran (cntlbar,i2,w6)");; 34 "CMUXn_IMP n (cntl:^wire,cntlbar:^wire,i1:^bus,i2:^bus,o:^bus) = 37 (cntl,cntlbar,DEST_BUS i1 m,DEST_BUS i2 m,DEST_BUS o m)");; 41 "MUXn_IMP n (cntl:^wire,i1:^bus,i2:^bus,o:^bus) = 43 INV_IMP (cntl,cntlbar) /\ CMUXn_IMP n (cntl,cntlbar,i1,i2,o)");; 77 "!cntl cntlbar i1 i2 [all...] |
/seL4-l4v-master/HOL4/examples/bmark/ |
H A D | Bmark.sml | 241 def = --`(MULT_FUN_CURRY 0 i1 i2 m t = 242 (if t then (m,0,t) else (if i1=0 then m else i2+m,0,T))) 244 (MULT_FUN_CURRY (SUC n) i1 i2 m t = 246 else MULT_FUN_CURRY n i1 i2 (if i1=0 then m else i2+m) 247 (((n-1)=0) \/ (i2=0))))`--}; 257 * --`!i1 i2 m n t. 258 * MULT_FUN_CURRY n i1 i2 m t = 260 * else MULT_FUN_CURRY (n-1) i1 i2 (if i1=0 then m else i2 [all...] |
/seL4-l4v-master/HOL4/examples/PSL/regexp/ |
H A D | matcherScript.sml | 533 let (i2,t2,a2) = regexp2na r2 in 534 (i1 + i2 + 1, 536 if s <= i2 then t2 s x s' 537 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s' 538 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))), 539 \s. if s <= i2 then a2 s else a2 i2 /\ a [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Ordered.sml | 14 fun compare ((i1,j1),(i2,j2)) = 15 case Int.compare (i1,i2) of
|
H A D | NameArity.sml | 34 fun compare ((n1,i1),(n2,i2)) = 37 | EQUAL => Int.compare (i1,i2) 40 fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Ordered.sml | 14 fun compare ((i1,j1),(i2,j2)) = 15 case Int.compare (i1,i2) of
|
H A D | NameArity.sml | 34 fun compare ((n1,i1),(n2,i2)) = 37 | EQUAL => Int.compare (i1,i2) 40 fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | quoteScript.sml | 32 ���!i1 i2. (index_compare i1 i2 = EQUAL) = (i1 = i2)���, 42 val index_lt_def = Define ` index_lt i1 i2 = (index_compare i1 i2 = LESS) `;
|
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowserFrame.java | 19 MenuItem i1, i2; field in class:GraphBrowserFrame 25 i2.setEnabled(false); 28 i2.setEnabled(true); 109 m1.add(i2 = new MenuItem("Export to EPS")); 112 i2.addActionListener(this);
|
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowserFrame.java | 19 MenuItem i1, i2; field in class:GraphBrowserFrame 25 i2.setEnabled(false); 28 i2.setEnabled(true); 109 m1.add(i2 = new MenuItem("Export to EPS")); 112 i2.addActionListener(this);
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/cmos/ |
H A D | mk_XOR.ml | 30 i2-- | --- | ---------------------| |---o 70 i2---| | | ------- | -- | 157 "BAD_XOR(i1,i2,o) = 161 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3)");; 170 "GOOD_XOR(i1,i2,o) = 174 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3) /\ 175 PTRAN(i1,i2,o) /\ NTRAN(p3,i2, [all...] |
H A D | mk_cmos.ml | 141 "!i1:^sig. !i2:^sig. !o:^sig. 142 J(i1,i2,o) = !t. o t = (i1 t) U1 (i2 t)");;
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Rationals.sml | 74 fun rat_plus (rat (i1,j1)) (rat (i2,j2)) = 78 val (i,j) = ((i1 * d2) + (i2 * d1),(j1 * d2)) 82 fun rat_minus (rat (i1,j1)) (rat (i2,j2)) = 86 val (i,j) = ((i1 * d2) - (i2 * d1),(j1 * d2)) 90 fun rat_mult (rat (i1,j1)) (rat (i2,j2)) = 91 if ((i1 = zero) orelse (i2 = zero)) 94 and h = gcd (abs i2,j1) 95 val i = (i1 div g) * (i2 div h) 100 fun rat_div (rat (i1,j1)) (rat (i2,j2)) = 101 if (i2 [all...] |
/seL4-l4v-master/HOL4/tools/cmp/ |
H A D | cmp.sml | 22 val i2 = BinIO.inputN(is2, 1024) value 25 if i1 = i2 then
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_icacheScript.sml | 14 X86_ICACHE ((r,e,s,m,i):x86_state) ((r2,e2,s2,m2,i2):x86_state) = 17 (i2 = \addr. if addr IN insert then m addr else 44 THEN `?r2 e2 t2 m2 i2. t = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR] 53 ``X86_ICACHE (r,e,s,m,i) (r2,e2,s2,m2,i2) = 55 (r2,e2,s2,m2,i2) = (r,e,s,m,icache update m i)``, 84 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_icacheScript.sml | 14 X64_ICACHE ((r,e,s,m,i):x64_state) ((r2,e2,s2,m2,i2):x64_state) = 17 (i2 = \addr. if addr IN insert then m addr else 44 THEN `?r2 e2 t2 m2 i2. t = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR] 53 ``X64_ICACHE (r,e,s,m,i) (r2,e2,s2,m2,i2) = 55 (r2,e2,s2,m2,i2) = (r,e,s,m,icache update m i)``, 84 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | symbolic_semi_automatonScript.sml | 91 (* (s1,i1) is the current state, (s2,i2) is the next state *) 93 `IS_TRANSITION A s1 i1 s2 i2 = 94 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 s1, INPUT_RUN_STATE_UNION A i2 s2)`; 120 (!s1 i1 i2. EXISTS_AT_MOST_ONE s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 128 (!s1 i1 i2. ?s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 140 (!s1 i1 i2. ?!s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2)) 282 ?R_FUNC. !s1 s2 i1 i2 [all...] |
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | simpleSetCatScript.sml | 122 Spushout (A:'a set) (B:'b set) (C:'c set) f g (P:'p set,i1,i2) (:'d) <=> 123 shom f A B /\ shom g A C /\ shom i1 B P /\ shom i2 C P /\ 124 restr (i1 o f) A = restr (i2 o g) A /\ 127 ?!u. shom u P Q /\ restr (u o i1) B = j1 /\ restr (u o i2) C = j2 270 Spushout A B C f g (P,i1,i2) (:'d) /\ INJ h univ(:'e) univ(:'d) ==> 271 Spushout A B C f g (P,i1,i2) (:'e) 357 Spushout (A:'a set) (B:'b set) (C:'c set) f g (P : 'd set,i1,i2) (:'e) /\ 360 ?H. BIJ H P Q /\ restr (H o i1) B = j1 /\ restr (H o i2) C = j2 384 ���restr (qp' o j1) B = i1 /\ restr (qp' o j2) C = i2��� 387 qpat_x_assum ���_ = i2��� (SUBST_ALL_TA [all...] |
/seL4-l4v-master/HOL4/examples/computability/lambda/ |
H A D | prtermScript.sml | 94 fun i2 q = GEN_ALL (Q.INST [`f` |-> q] prf2) function 96 fun intro2 q = HO_MATCH_MP_TAC (i2 q) 307 SRW_TAC [][prCn2, i2 `ncons`] THEN 309 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN 312 SRW_TAC [][prDIV, i2 `$+`], 316 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN 318 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN 320 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`], 322 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN 324 SRW_TAC [][i2 `ne [all...] |
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | ARM_prover_toolsLib.sml | 98 val (rcs, i2) = dest_comb rcst 101 val (thm, _) = prove_it comp i1 i2 unt simp 181 COMB (rcs, i2) 186 if ((i2 ~~ ``mode_mix:(arm_state->bool)``) andalso ((unt ~~ ``priv_mode_constraints_v2a``) andalso (sim ~~ ``priv_mode_similar``))) 202 COMB (rcs, i2) 206 COMB (rel, comp) => if (i2 ~~ ``little_mode_mix:(arm_state->bool)``)
|