Searched refs:temp (Results 1 - 25 of 46) sorted by relevance

12

/seL4-l4v-master/seL4/include/arch/arm/arch/model/
H A Dsmp.h22 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 Dselftest.sml3 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 Dmachine.h130 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 DTemp.sml3 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 DTree.sml15 | TEMP of Temp.temp
50 | TEMP of Temp.temp
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DTemp.sml3 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 DTree.sml15 | TEMP of Temp.temp
50 | TEMP of Temp.temp
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DTemp.sml3 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 DTree.sml15 | TEMP of Temp.temp
/seL4-l4v-master/seL4/include/arch/arm/arch/64/mode/machine/
H A Dfpu.h17 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 Dcodegen_armLib.sml63 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 Dreg_allocLib.sml101 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 Driscv_plic0.h64 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 Dproblem-set-1-answers.lisp648 (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 DtempScript.sml41 val _ = new_theory "temp";
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/
H A Dmachine.h224 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 Disabelle_system.scala85 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 Disabelle_system.scala85 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 Dlisp_compiler_opScript.sml1165 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 DConsThms.sml79 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 DwardScript.sml133 val temp' = insert cmp (es,v) (empty cmp)
135 Node(valopt, Binarymap.insert(d,e,temp'))
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheoryPP.sml34 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 Dmips.sml3742 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 DminisatProve.sml80 (* cleanup temp files. this won't work fully if we cannot delete files
/seL4-l4v-master/HOL4/src/list/examples/
H A Dtest.sml377 new_theory "temp";

Completed in 313 milliseconds

12