| /seL4-l4v-10.1.1/seL4/include/smp/ |
| H A D | ipi.h | 88 * @param data1 passed to the function as first parameter
92 void doRemoteMaskOp(IpiRemoteCall_t func, word_t data1, word_t data2, word_t data3, word_t mask);
97 * @param data1 passed to the function as first 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));
124 doRemoteMaskOp1Arg(IpiRemoteCall_t func, word_t data1, word_t mask)
126 doRemoteMaskOp(func, data1, 0, 0, mask);
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_
[all...] |
| /seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
| H A D | globinits.c | 22 int data1; member in struct:s
34 x += i + y + sptr->data1 + array[i] + *z;
40 return sval.data1 + svalprime.data2;
|
| /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,
27 ipi_args[0] = data1;
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,
27 ipi_args[0] = data1;
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 | 32 uint8_t data1; 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.
3126 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data1)) sfb_split)
3129 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data1)) sfb_context)
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.
3170 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data1)) sfb_split)
3173 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data1)) sfb_context)
3176 (data1 = data2)) sfb_imp)) sfb_restP)``,
4235 Q.ABBREV_TAC `data1
[all...] |
| H A D | holfootLib.sml | 2281 val (i1, (e, ne, data1)) = dest_holfoot_ap_data_array_interval ttt;
2293 (true, try_split context i2 i1 (ec2,nc2) (ec1, nc1, data1))
2987 Cases_on `n_const = LENGTH data1` THEN
3000 Cases_on `data1 = []`
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
| H A D | lalr.sml | 296 fun dfs(a as ((key1,data1),r)) =
299 NTL.insert((key1,Look.union(data1,data2)),r)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscv.sml | 98 { addr: BitsN.nbit option, data1: BitsN.nbit option,
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, data
[all...] |
| H A D | riscv.sig | 98 { addr: BitsN.nbit option, data1: BitsN.nbit option,
|
| H A D | riscvScript.sml | 116 [("addr",OTy F64),("data1",OTy F64),("data2",OTy F64),
4216 ("data1",
4274 ("data1",
12012 ("data1",
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
| H A D | riscv.spec | 1243 data1 :: regType option -- data result for instruction:
1270 ; Delta.data1 <- None
1279 ; Delta.data1 <- Some(val)
1606 ; when not PROVER_EXPORT do Delta.data1 <- Some(val)
1627 ; Delta.data1 <- Some(ZeroExtend(val))
1634 ; Delta.data1 <- Some(val)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8.sml | 1829 val data1 = value
1841 write'Mem N (data1,x)
1854 val (data1,data2) = value
1863 then ( write'X 64 (ExtendWord (64,64) (data1,signed),t)
1866 else ( write'X N (data1,t); write'X N (data2,t2) )
|
| H A D | arm8Script.sml | 1952 Let(TP[Var("data1",BTy"N"),
1972 TP[Var("data1",
1986 TP[Var("data1",BTy"N"),
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_opsemScript.sml | 3288 (\(data1,data2).
3290 write_reg ii rt data1 |||
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
| H A D | arm_opsemScript.sml | 3311 (\(data1,data2).
3313 write_reg ii rt data1 |||
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/monadic-arm/ |
| H A D | armScript.sml | [all...] |