/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/errors/ |
H A D | addrlocal.c | 11 void swap(int *i1, int *i2) argument 14 tmp = *i1; 15 *i1 = *i2;
|
/seL4-l4v-10.1.1/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) = 19 NAND_SPEC(c,i1,l3) /\
|
/seL4-l4v-10.1.1/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),((i1 [all...] |
H A D | mk_COUNT.ml | 23 "MUX(switch,i1:^sig,i2:^sig,o:^sig) = (o = (switch -> i1 | i2))");;
|
/seL4-l4v-10.1.1/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) = 38 Ptran (i1,w1,w2) /\ 42 Ntran (i1,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) = 24 Ptran (cntlbar,i1,w1) /\ 25 Ntran (cntl,i1,w2) /\ 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 i [all...] |
/seL4-l4v-10.1.1/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) `; 53 /\ (varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) 54 /\ (varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1)
|
/seL4-l4v-10.1.1/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) 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+m) 269 --`!i1 i [all...] |
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/examples/STE/Examples/ |
H A D | And.sml | 8 (s_b' node = ((s_b "i0") /\ (s_b "i1"))))`; 13 else if (node = "i1") then X 16 And (s "i0")(s "i1") 23 val a2 = (T, "i1", ``v2:bool``, 0, 1); 45 val a2 = (T, "i1", ``v2:bool``, 0, 1);
|
H A D | Or.sml | 7 (s_b' node = ((s_b "i0") \/ (s_b "i1"))))`; 12 else if (node = "i1") then X 15 Or (s "i0")(s "i1") 22 val a2 = (T, "i1", ``v2:bool``, 0, 1); 48 val a2 = (T, "i1", ``v2:bool``, 0, 1);
|
H A D | Comparator-for-STE-Reduction.sml | 33 else if (node = "i1") 46 else if (node = "i1") then 50 And (s "i0")(s "i1") 60 else if (node = "i1") then Xnor (s "a1")(s "b1") 111 B2 = ("i1" is 1) from 1 to 2 148 val B2 = (T, "i1", T, 0, 1); 157 val B2 = (T, "i1", T, 1, 2);
|
/seL4-l4v-10.1.1/HOL4/tools/cmp/ |
H A D | cmp.sml | 20 val i1 = BinIO.inputN(is1, 1024) value 25 if i1 = i2 then 26 if Word8Vector.length i1 > 0 then recurse()
|
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowserFrame.java | 19 MenuItem i1, i2; field in class:GraphBrowserFrame 24 i1.setEnabled(false); 27 i1.setEnabled(true); 108 m1.add(i1 = new MenuItem("Export to PostScript")); 111 i1.addActionListener(this);
|
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowserFrame.java | 19 MenuItem i1, i2; field in class:GraphBrowserFrame 24 i1.setEnabled(false); 27 i1.setEnabled(true); 108 m1.add(i1 = new MenuItem("Export to PostScript")); 111 i1.addActionListener(this);
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/cmos/ |
H A D | mk_XOR.ml | 22 i1---+---- | ---------------------------| 64 i1------+---- | ------+--------------------| 157 "BAD_XOR(i1,i2,o) = 160 PTRAN(i1,p1,p3) /\ NTRAN(i1,p3,p2) /\ 161 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3)");; 170 "GOOD_XOR(i1,i2,o) = 173 PTRAN(i1,p1,p3) /\ NTRAN(i1,p3,p2) /\ 174 PTRAN(i2,i1, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/ |
H A D | matcherScript.sml | 534 let (i1,t1,a1) = regexp2na r1 in 536 (i1 + i2 + 1, 543 let (i1,t1,a1) = regexp2na r1 in 545 (i1 + i2 + 1, 552 let (i1,t1,a1) = regexp2na r1 in 554 (i1 + i2 + 2, 556 if s = i1 + i2 + 2 then 557 if s' <= i1 then t1 i1 x s' else t2 i2 x (s' - (i1 [all...] |
/seL4-l4v-10.1.1/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)) 93 else let val g = gcd (abs i1,j2) 95 val i = (i1 div g) * (i2 div h) 100 fun rat_div (rat (i1,j1)) (rat (i2,j2)) = 102 else if (i1 [all...] |
H A D | Sol_ranges.sml | 84 let val i1 = upper_int_of_rat r1 value 86 in not (i2 < i1) 101 (let val i1 = upper_int_of_rat r1 value 103 val i1' = if (i1 < zero) then zero else i1 104 in if (i2 < i1') then failwith "fail" else i1'
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | selftest.sml | 14 fun m10cmp (i1,i2) = Int.compare(i1 mod 10, i2 mod 10)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | jrhCore.sml | 40 ``!i1 i2 x. ((x = i1) = eval_form (xEQ i1) x) /\ 41 (x < i1 = eval_form (xLT i1) x) /\ 42 (i1 int_divides x + i2 = eval_form (xDivided i1 i2) x)``, 199 (eval_form (neginf (xDivided i1 i2)) x = i1 int_divides x + i2)``, 211 (eval_form (posinf (xDivided i1 i [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | symbolic_semi_automatonScript.sml | 115 `(IS_TRANSITION A s1 i1 s2 i2 = 116 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 s1, INPUT_RUN_STATE_UNION A i2 s2))`; 154 (!s1 i1 i2. EXISTS_AT_MOST_ONE s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 161 (!s1 i1 i2. ?s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 175 (!s1 i1 i2. ?!s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))``, 351 ``!A. IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A ==> ?R_FUNC. !s1 s2 i1 i2. (R_FUNC s1 i1 i [all...] |