| /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...] |