| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | arm_evalLib.sml | 638 val data = inputAll istr value
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/mlton/ |
| H A D | updateML.sml | 21 datatype data = Byte of word8 | Half of word16 | Word of word32 type
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/executable-semantics/ |
| H A D | test.v | 55 reg [31:0] data; // Data last read from Sender register
96 reg [31:0] data; // Data last read from BUF register
[all...] |
| H A D | test2.v | 65 reg [31:0] data; // Data last read from Sender register
112 reg [31:0] data; // Data last read from BUF register
[all...] |
| H A D | test_c.v | 52 reg [31:0] data; // Data last read from Sender register
92 reg [31:0] data; // Data last read from BUF register
[all...] |
| H A D | test_c1.v | 56 reg [31:0] data; // Data last read from Sender register
94 reg [31:0] data; register
[all...] |
| H A D | test_c2.v | 52 reg [31:0] data; // Data last read from Sender register
92 reg [31:0] data; // Data last read from BUF register
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | funCall.sml | 498 val data = map (fn (dest, src) => (dest, src, direct_before dest)) regL value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | fieldTools.sml | 986 val data = value
1149 val data = value
1211 val data = value
|
| /seL4-l4v-10.1.1/HOL4/examples/imperative/ |
| H A D | necec2010.sml | 29 we enable the HOL system to display all assumptions and data types currently in use. structure
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 4987 val data = MemU 32 (address,4) value
5016 val data = MemU 32 (address,4) value
5049 val data = MemU_unpriv 32 (address,4) value
5149 val data = MemU 16 (address,2) value
5167 val data = MemU 16 (address,2) value
5189 val data = MemU_unpriv 16 (address,2) value
5438 val data = value
5468 val data = value
5805 val data = MemA 8 (Rn,1) value
5816 val data = MemA 32 (Rn,4) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8.sml | 1215 val data = value
1747 val data = if rt_unknown then BitsN.fromNat(0,N) else X N t value
1755 val data = value
1909 val data = if rt_unknown then BitsN.fromNat(0,N) else X N t value
1935 val data = Mem N (address,(dbytes,acctype)) value
1962 val data = value
2000 val data = Mem N (address,(dbytes,acctype)) value
2031 val data = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0.sml | 1571 val data = MemU 32 (address,4) value
1595 val data = MemU 8 (address,1) value
1611 val data = MemU 16 (address,2) value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscv.sml | 3864 val data = MEM pAddrIdx value
3874 val data = BitsN.bits(63,0) ddw value
3962 val data = MEM pAddrIdx value
5644 val data = GPR rs2 value
5675 val data = GPR rs2 value
5706 val data = GPR rs2 value
5739 val data = GPR rs2 value
5837 val data = GPR rs2 value
5896 val data = GPR rs2 value
5946 val data = GPR rs2 value
5995 val data = GPR rs2 value
6046 val data = GPR rs2 value
6102 val data = GPR rs2 value
6160 val data = GPR rs2 value
6216 val data = GPR rs2 value
6274 val data = GPR rs2 value
6330 val data = GPR rs2 value
6388 val data = GPR rs2 value
6444 val data = GPR rs2 value
6502 val data = GPR rs2 value
6558 val data = GPR rs2 value
6616 val data = GPR rs2 value
6672 val data = GPR rs2 value
6730 val data = GPR rs2 value
6786 val data = GPR rs2 value
6844 val data = GPR rs2 value
6900 val data = GPR rs2 value
6980 val data = FPRS rs2 value
7472 val data = FPRD rs2 value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
| H A D | hashtbl.h | 28 hashData data; member in class:hashElement
|
| H A D | slist.h | 25 void *data; member in class:voidSList::voidSListElem
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | bddio.c | 56 int data; member in struct:s_LoadHash
566 static void loadhash_add(int key, int data) argument
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 1105 val (data, _) = dest_forall (rhs (concl xthm4)) value
2376 val data = listSyntax.mk_list (rev upL', pairSyntax.mk_prod ( value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 453 val data = map gen_data names value
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | BasicStreamIO.sml | 124 val data = readVec chunkSize value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/msvc32include/ |
| H A D | ffi.h | 264 char data[FFI_SIZEOF_ARG];
member in union:__anon28
275 char data[FFI_SIZEOF_JAVA_RAW];
member in union:__anon29
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | polyffi.cpp | 492 static void callbackEntryPt(ffi_cif *cif, void *ret, void* args[], void *data) argument
|
| H A D | xwindows.cpp | 2510 PolyWord data; /* ML (abstype containing) string */ member in struct:__anon90
2544 PolyStringObject *data = GetString(I->data); local
3143 PolyWord data; /* pointer to event-specific data, i member in class:ML_Event
3189 #define data macro
3197 #undef data macro
3222 #define data macro
3232 #undef data macro
3242 #define data macro
3250 #undef data macro
3265 #define data macro
3273 #undef data macro
3286 #define data macro
3296 #undef data macro
3329 #define data macro
3332 #undef data macro
3349 #define data macro
3353 #undef data macro
3371 #define data macro
3378 #undef data macro
3392 #define data macro
3395 #undef data macro
3414 #define data macro
3420 #undef data macro
3439 #define data macro
3442 #undef data macro
3453 #define data macro
3456 #undef data macro
3475 #define data macro
3480 #undef data macro
3492 #define data macro
3499 #undef data macro
3510 #define data macro
3513 #undef data macro
3532 #define data macro
3535 #undef data macro
3546 #define data macro
3549 #undef data macro
3560 #define data macro
3564 #undef data macro
3581 #define data macro
3584 #undef data macro
3595 #define data macro
3600 #undef data macro
3611 #define data macro
3617 #undef data macro
3691 #define data macro
3696 #undef data macro
3759 #define data macro
3766 #undef data macro
3791 #define data macro
3804 #undef data macro
3976 Handle data; local
4023 #define data macro
4029 #undef data macro
4303 #define data macro
4308 #undef data macro
5004 #define data macro
5011 #undef data macro
5048 #define data macro
5062 #undef data macro
5238 #define data macro
5243 #undef data macro
5261 #define data macro
5266 #undef data macro
5299 #define data macro
5304 #undef data macro
5512 #define data macro
5520 #undef data macro
5550 #define data macro
5560 #undef data macro
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | ThmSetData.sig | 4 type data = Theory.LoadableThyData.t type
|
| H A D | ThmSetData.sml | 6 type data = LoadableThyData.t type
104 val (data, _) = mk' [s] value
172 val (data, namedthm value
[all...] |