/seL4-l4v-master/HOL4/src/integer/testing/ |
H A D | tcooper.c | 73 struct timeval tv; local 79 select(pipe_fds[0] + 1, &to_watch, 0, 0, &tv); 83 /* need to do this potentially redundant assignment to tv because 84 select leaves the value of tv undefined */ 85 tv.tv_sec = timeout; 86 tv.tv_usec = 0; 87 retval = select(pipe_fds[0] + 1, &to_watch, 0, 0, &tv);
|
/seL4-l4v-master/isabelle/Admin/bash_process/ |
H A D | bash_process.c | 26 struct timeval tv; local 27 if (gettimeofday(&tv, NULL) == 0) { 28 return tv.tv_sec * 1000 + tv.tv_usec / 1000;
|
/seL4-l4v-master/l4v/isabelle/Admin/bash_process/ |
H A D | bash_process.c | 26 struct timeval tv; local 27 if (gettimeofday(&tv, NULL) == 0) { 28 return tv.tv_sec * 1000 + tv.tv_usec / 1000;
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | locking.cpp | 202 struct timeval tv; local 203 if (gettimeofday(&tv, NULL) != 0) 205 waitTime.tv_sec = tv.tv_sec + milliseconds / 1000; 206 waitTime.tv_nsec = (tv.tv_usec + (milliseconds % 1000) * 1000) * 1000;
|
H A D | timing.cpp | 219 struct timeval tv; 220 if (gettimeofday(&tv, NULL) != 0) 222 result = Make_arb_from_pair_scaled(taskData, tv.tv_sec, tv.tv_usec, 1000000); 549 struct timeval tv; 550 if (gettimeofday(&tv, NULL) != 0) 552 subTimevals(&tv, &startTime); 553 result = Make_arb_from_pair_scaled(taskData, tv.tv_sec, tv.tv_usec, 1000000);
|
H A D | heapsizing.cpp | 659 struct timeval tv; 660 if (gettimeofday(&tv, NULL) != 0) 662 realTime = tv; 850 struct timeval tv; 851 if (getrusage(RUSAGE_SELF, &rusage) != 0 || gettimeofday(&tv, NULL) != 0) 855 realTime.add(tv);
|
H A D | statistics.cpp | 670 struct timeval tv; 672 gettimeofday(&tv, NULL); 675 subTimevals(&tv, &startTime); 676 subTimevals(&tv, &gcRealTime); 679 setTimeValue(PST_NONGC_RTIME, tv.tv_sec, tv.tv_usec);
|
/seL4-l4v-master/l4v/tools/autocorres/tests/examples/ |
H A D | schorr_waite.c | 88 struct timeval tv; local 89 if (gettimeofday(&tv, NULL)) { 92 unsigned long long t = (unsigned long long)tv.tv_sec * 1000000 + tv.tv_usec;
|
/seL4-l4v-master/HOL4/examples/algebra/linear/ |
H A D | SpanSpaceScript.sml | 532 (2) k <> 0 ==> h' o h || v = h' o h || tv || EL k (h'::t) o EL k (h::b) || dv 533 where tv = (TAKE (k - 1) t) |o| (TAKE (k - 1) b) 536 Hence v = tv || EL j t o EL j b || dv by induction hypothesis 549 Hence tv IN V /\ dv IN V by vspace_span_vector 552 h' o h || tv || EL k (h'::t) o EL k (h::b) || dv 553 = h' o h || tv || ej || dv 554 = h' o h || tv || (ej || dv) by group_assoc 555 = h' o h || (tv || ej || dv by group_assoc 573 qabbrev_tac `tv = (TAKE (k - 1) t) |o| (TAKE (k - 1) b)` >> 577 `v = tv || E [all...] |
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 124 else let val b1 = List.map (fn (vi,tv) => if tv then bdd.ithvar vi else bdd.nithvar vi) 125 (List.filter (fn (vi,tv) => Option.isSome(getVarForInt vm vi))
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | unifyTools.sml | 46 fun occurs tv ty = mem tv (type_vars ty)
|
/seL4-l4v-master/HOL4/examples/HolBdd/ |
H A D | PrimitiveBddRules.sml | 495 fun BddCon tv vm = 496 if tv then TermBdd(HolBddTag,Term.empty_tmset,vm,T,bdd.TRUE) 513 fun BddVar tv vm v = 515 SOME n => if tv 821 (fn (n,tv) => 827 if tv then T else F))
|
H A D | DerivedBddRules.sml | 691 (fn (n,tv) => ((case assoc2 n vml of 695 BddCon tv vm)) 902 (fn (n,tv) => 907 if tv then T else F))
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 1472 val () = #apply explicit(fn (_, tv) => setTvarLevel (tv, newLevel)); 1479 (fn (name, tv) => 1480 case #lookupTvars env name of SOME v => linkTypeVars(v, tv) | NONE => setTvarLevel (tv, newLevel)); 1622 #apply explicit(fn (_, tv) => setTvarLevel (tv, funLevel)); 1629 (fn (name, tv) => 1630 case #lookupTvars env name of SOME v => linkTypeVars(v, tv) | NONE => setTvarLevel (tv, funLeve [all...] |
H A D | CODEGEN_PARSETREE.sml | 301 val filterTypeVars = List.filter (fn tv => not justForEqualityTypes orelse tvEquality tv) 1182 fun checkVars tv = 1183 case List.find(fn t => sameTv(t, tv)) fdTypeVars of
|
/seL4-l4v-master/HOL4/src/opentheory/postbool/ |
H A D | Logging.sml | 528 val (tv,tb) = dest_abs template value 529 val vv = prim_variant (HOLset.listItems fvs) tv 531 val tb = subst [tv|->vv] tb
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 1088 val tv = boolSyntax.mk_eq (l, v) value 1090 if List.exists (aconv tv) rst
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 221 val filterTypeVars = List.filter (fn tv => not TYPEIDCODE.justForEqualityTypes orelse tvEquality tv)
|
H A D | TYPEIDCODE.sml | 151 SOME (tv, _) => SOME(TypeVar tv)
|