/seL4-l4v-master/seL4/include/arch/arm/arch/model/ |
H A D | smp.h | 22 void *temp; local 27 : [atomic_var] "=&r"(atomic_status), [prev_output]"=&r"(temp) /* output */ 32 *prev = temp;
|
/seL4-l4v-master/HOL4/tools/quote-filter/ |
H A D | selftest.sml | 3 val _ = system "./quote-filter input temp-output" 5 val result = system "diff temp-output desired-output"
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/ |
H A D | machine.h | 130 word_t temp; local 131 asm volatile("csrr %0, stval" : "=r"(temp)); 132 return temp; 137 word_t temp; local 138 asm volatile("csrr %0, scause" : "=r"(temp)); 139 return temp; 144 word_t temp; local 145 asm volatile("csrr %0, sepc" : "=r"(temp)); 146 return temp; 151 word_t temp; local 160 word_t temp; local 167 word_t temp; local 173 word_t temp; local [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | Temp.sml | 3 eqtype temp 4 val newtemp : unit -> temp 5 structure Table : TABLE sharing type Table.key = temp 6 val makestring: temp -> string 16 type temp = int type
|
H A D | Tree.sml | 15 | TEMP of Temp.temp 50 | TEMP of Temp.temp
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | Temp.sml | 3 eqtype temp 4 val newtemp : unit -> temp 5 structure Table : TABLE sharing type Table.key = temp 6 val makestring: temp -> string 16 type temp = int type
|
H A D | Tree.sml | 15 | TEMP of Temp.temp 50 | TEMP of Temp.temp
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | Temp.sml | 3 eqtype temp 4 val newtemp : unit -> temp 5 structure Table : TABLE sharing type Table.key = temp 6 val makestring: temp -> string 14 type temp = int type
|
H A D | Tree.sml | 15 | TEMP of Temp.temp
|
/seL4-l4v-master/seL4/include/arch/arm/arch/64/mode/machine/ |
H A D | fpu.h | 17 word_t temp; local 43 : "=&r"(temp) 52 word_t temp; local 78 : "=&r"(temp)
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sml | 63 val temp = get_arm_temp_reg () value 67 ["add? " ^ r temp ^ ", " ^ r d ^ ", #" ^ Arbnum.toString i ] @ swpb (ASSIGN_ADDRESS_REG temp,j) 69 ["sub? " ^ r temp ^ ", " ^ r d ^ ", #" ^ Arbnum.toString i ] @ swpb (ASSIGN_ADDRESS_REG temp,j) 82 | f (ASSIGN_STACK (i,ASSIGN_X_CONST j)) = assign_const_to_reg j temp @ ["str? " ^ r temp ^ ", " ^ s i] 84 | f (ASSIGN_MEMORY (ACCESS_WORD,a,ASSIGN_X_CONST i)) = assign_const_to_reg i temp @ ["str? " ^ r temp ^ ", " ^ address a]
|
H A D | reg_allocLib.sml | 101 val temp = mk_temp_var ty value 102 val temp = if ty = ``:word32`` then temp else value 104 handle HOL_ERR _ => temp 105 in divide_aux g (xs @ [(temp,t)], subst [t |-> temp] rhs) end
|
/seL4-l4v-master/seL4/include/drivers/irq/ |
H A D | riscv_plic0.h | 64 word_t temp; local 65 asm volatile("csrr %0, sie" : "=r"(temp)); 66 return temp;
|
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | problem-set-1-answers.lisp | 648 (let ((temp (mod x (expt 2 n)))) 649 (if (< temp (expt 2 (- n 1))) 650 temp 651 (- temp (expt 2 n)))))
|
/seL4-l4v-master/HOL4/examples/ |
H A D | tempScript.sml | 41 val _ = new_theory "temp";
|
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/ |
H A D | machine.h | 224 word_t temp; local 227 "movabs $1f, %[temp] \n" 228 "movq %[temp], (%[returnto_addr]) \n\ 234 [temp] "=&r"(temp),
|
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 85 val temp = if (Platform.is_windows) System.getenv("TEMP") else null 86 if (temp != null && temp.contains('\\')) temp else ""
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 85 val temp = if (Platform.is_windows) System.getenv("TEMP") else null 86 if (temp != null && temp.contains('\\')) temp else ""
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_compiler_opScript.sml | 1165 x0 -- temp 1939 BC_expand_macro (temp:SExp,task,exp,a,ret,consts,xs) = 1940 let temp = exp in 1943 let exp = Dot (Sym "CAR") (CDR temp) in 1946 let exp = Dot (Sym "FIRST") (Dot (Dot (Sym "CDR") (CDR temp)) (Sym "NIL")) in 1949 let exp = Dot (Sym "SECOND") (Dot (Dot (Sym "CDR") (CDR temp)) (Sym "NIL")) in 1952 let exp = Dot (Sym "THIRD") (Dot (Dot (Sym "CDR") (CDR temp)) (Sym "NIL")) in 1955 let exp = Dot (Sym "FOURTH") (Dot (Dot (Sym "CDR") (CDR temp)) (Sym "NIL")) in 1959 let (nil,vars,exps,zero,xs) = mc_map_car (CAR (CDR temp), exp, exp, exp, xs) in 1960 let lam = Dot (Sym "LAMBDA") (Dot vars (Dot (CAR (CDR (CDR temp))) (Sy [all...] |
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sml | 79 val temp = map strip_forall value 83 val applied_cons_list = map (fn x => rand (lhs (snd x))) temp 88 val temp = map (map (fn x => decompose (x, []))) divided_list value 90 val cons_var_list = map split temp 279 val temp = map strip_forall value 283 val applied_cons_list = map (fn x => rand (lhs (snd x))) temp 289 val temp = map (map (fn x => decompose (x, []))) divided_list value 291 val unsplit_cons_var_list = map (filter (fn x => snd x <> [])) temp
|
/seL4-l4v-master/HOL4/examples/misc/ |
H A D | wardScript.sml | 133 val temp' = insert cmp (es,v) (empty cmp) 135 Node(valopt, Binarymap.insert(d,e,temp'))
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | TheoryPP.sml | 34 val temp_binding_pfx = "@temp" 40 else raise ERR "dest_temp_binding" "String not a temp-binding"
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mips.sml | 3742 val temp = value 3745 if not((BitsN.bit(temp,32)) = (BitsN.bit(temp,31))) 3747 else write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rt) 3756 val temp = value 3759 write'GPR(BitsN.signExtend 64 temp,rt) 3765 val temp = value 3768 if not((BitsN.bit(temp,64)) = (BitsN.bit(temp,63))) 3770 else write'GPR(BitsN.bits(63,0) temp,r 3801 val temp = value 3815 val temp = value 3827 val temp = value 3841 val temp = value 3850 val temp = value 3862 val temp = value 3897 val temp = value 3915 val temp = value 3933 val temp = value 3951 val temp = value 4277 val temp = value 4329 val temp = value 4733 val temp = GPR rs value 4760 val temp = GPR rs value 4769 val temp = GPR rs value 4796 val temp = GPR rs value 4805 val temp = GPR rs value [all...] |
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | minisatProve.sml | 80 (* cleanup temp files. this won't work fully if we cannot delete files
|
/seL4-l4v-master/HOL4/src/list/examples/ |
H A D | test.sml | 377 new_theory "temp";
|