| /seL4-l4v-master/HOL4/src/1/theory_tests/ |
| H A D | addMLdep2Script.sml | 8 val instr = TextIO.openIn fname value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | Assem.sml | 35 datatype instr = OPER of {oper: operation * cond option * bool, type
|
| H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} type
|
| H A D | regAllocation.sml | 624 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)) value
644 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
659 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | Assem.sml | 35 datatype instr = OPER of {oper: operation * cond option * bool, type
|
| H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} type
|
| H A D | regAllocation.sml | 624 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)) value
644 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
659 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | Assem.sml | 35 datatype instr = OPER of {oper: operation * cond option * bool, type
|
| H A D | IRSyntax.sml | 33 type instr = {oper: operator, dst: exp list, src: exp list} type
|
| H A D | regAllocation.sml | 624 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)) value
644 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
659 val {instr = curInst, def = df, use = us} = #3 (G.context(nodeNo,gr)); value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | SALGen.sml | 75 val instr = list_mk_comb (inst [alpha |-> ty] asg_tm, [entry_l, dest, src, exit_l]) value
|
| /seL4-l4v-master/HOL4/tools-poly/poly/ |
| H A D | Help.sml | 111 fun instr s str = function
|
| /seL4-l4v-master/HOL4/developers/ |
| H A D | comparelogs.sml | 54 val instr = TextIO.openIn fname value
|
| /seL4-l4v-master/HOL4/help/src-sml/ |
| H A D | makebase.sml | 195 let val instr = TextIO.openIn value
|
| /seL4-l4v-master/HOL4/tools/ |
| H A D | configure.sml | 132 val instr = BinIO.openIn src value
|
| H A D | buildutils.sml | 753 val instr = TextIO.openIn(fullPath [HOLDIR, "tools", value
|
| /seL4-l4v-master/HOL4/tools-poly/ |
| H A D | configure.sml | 152 val instr = BinIO.openIn src value
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | Holmake_tools.sml | 733 val instr = openIn (normPath s) value
|
| /seL4-l4v-master/HOL4/examples/ARM/v7/ |
| H A D | arm_parserLib.sml | 3843 (let val instr = mk_Hint (mk_Hint_debug (mk_word4 v)) in value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 4111 val instr = value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscv.sig | 1065 val instr: string -> string value
|
| H A D | riscv.sml | 13600 fun instr o' = L3.padRightString(#" ",(12,o')); function
[all...] |