/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | globinits.c | 23 char data2; member in struct:s 30 s_t sval = {.data2 = 3}, svalprime; 40 return sval.data1 + svalprime.data2;
|
/seL4-l4v-10.1.1/seL4/include/smp/ |
H A D | ipi.h | 89 * @param data2 passed to the function as second parameter 92 void doRemoteMaskOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask); 98 * @param data2 passed to the function as second parameter 101 static void inline doRemoteOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t cpu) 103 doRemoteMaskOp(func, data1, data2, data3, BIT(cpu)); 130 doRemoteMaskOp2Arg(IpiRemoteCall_t func, word_t data1, word_t data2, word_t mask) 132 doRemoteMaskOp(func, data1, data2, 0, mask); 136 doRemoteMaskOp3Arg(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) 138 doRemoteMaskOp(func, data1, data2, data3, mask); 153 doRemoteOp2Arg(IpiRemoteCall_t func, word_t data1, word_t data2, word_ [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/arm/smp/ |
H A D | ipi.c | 23 word_t data1, word_t data2, word_t data3, 28 ipi_args[1] = data2; 22 init_ipi_args(IpiModeRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) argument
|
/seL4-l4v-10.1.1/seL4/src/smp/ |
H A D | ipi.c | 87 void doRemoteMaskOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) argument 95 init_ipi_args(func, data1, data2, data3, mask);
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/smp/ |
H A D | ipi.c | 23 word_t data1, word_t data2, word_t data3, 28 ipi_args[1] = data2; 22 init_ipi_args(IpiModeRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask) argument
|
/seL4-l4v-10.1.1/l4v/tools/asmrefine/testfiles/ |
H A D | global_array_swap.c | 33 uint8_t data2; member in struct:struct_blob
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootScript.sml | 3121 ``!wpb rpb e tagL dtagL data1 data2 sfb_context sfb_split sfb_imp. 3127 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data2)) sfb_imp) 3132 (data1 = data2)) sfb_imp))``, 3135 Cases_on `data2 = data1` THEN1 ( 3165 ``!wpb rpb e tagL dtagL data1 data2 sfb_context sfb_split sfb_imp sr wpb' sfb_restP. 3171 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data2)) sfb_imp) sfb_restP) = 3176 (data1 = data2)) sfb_imp)) sfb_restP)``, 4236 Q.ABBREV_TAC `data2 = (MAP (\x. (FST x,DROP (SUC n) (SND x))) data)` THEN 4237 `ALL_DISTINCT (tl::MAP FST data1) /\ ALL_DISTINCT (tl::MAP FST data2)` by ( 4238 Q.UNABBREV_TAC `data1` THEN Q.UNABBREV_TAC `data2` THE [all...] |
H A D | holfootLib.sml | 2213 fun try_split context i1 i2 (ec1,nc1) (ec2,nc2,data2) = 2245 val xthm4 = SPEC data2 xthm3 2286 val (i2, (e', ne', data2)) = dest_holfoot_ap_data_array_interval tttt 2292 (false, try_split context i1 i2 (ec1,nc1) (ec2, nc2, data2)) handle HOL_ERR _ =>
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | lalr.sml | 298 of SOME (_,data2) => 299 NTL.insert((key1,Look.union(data1,data2)),r)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | problem.py | 323 for (data2, va) in self.loop_var_analysis_cache[k]: 324 if data2 == data:
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
H A D | riscv.sml | 99 data2: BitsN.nbit option, exc_taken: bool, fetch_exc: bool, 1323 fun StateDelta_addr_rupd ({addr, data1, data2, exc_taken, fetch_exc, 1325 {addr = x', data1 = data1, data2 = data2, exc_taken = exc_taken, 1329 fun StateDelta_data1_rupd ({addr, data1, data2, exc_taken, fetch_exc, 1331 {addr = addr, data1 = x', data2 = data2, exc_taken = exc_taken, 1335 fun StateDelta_data2_rupd ({addr, data1, data2, exc_taken, fetch_exc, 1337 {addr = addr, data1 = data1, data2 = x', exc_taken = exc_taken, 1341 fun StateDelta_exc_taken_rupd ({addr, data1, data2, exc_take [all...] |
H A D | riscv.sig | 99 data2: BitsN.nbit option, exc_taken: bool, fetch_exc: bool,
|
H A D | riscvScript.sml | 116 [("addr",OTy F64),("data1",OTy F64),("data2",OTy F64), 4107 ("data2", 12034 ("data2",
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 1247 data2 :: regType option -- data argument for instruction: 1271 ; Delta.data2 <- None 1285 ; Delta.data2 <- Some(val) 1586 Delta.data2 <- Some(CSR(csr)) -- Note that writes to CSR are intercepted
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8.sml | 1833 val data2 = value 1848 write'Mem N (data2,x) 1854 val (data1,data2) = 1864 ; write'X 64 (ExtendWord (64,64) (data2,signed),t2) 1866 else ( write'X N (data1,t); write'X N (data2,t2) )
|
H A D | arm8Script.sml | 1953 Var("data2",BTy"N")], 1961 TP[Var("data2", 1980 TP[Var("data2",BTy"N"),
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_opsemScript.sml | 3288 (\(data1,data2). 3291 write_reg ii rt2 data2) >>=
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_opsemScript.sml | 3311 (\(data1,data2). 3314 write_reg ii rt2 data2) >>=
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/monadic-arm/ |
H A D | armScript.sml | [all...] |