Searched refs:tv (Results 1 - 19 of 19) sorted by relevance

/seL4-l4v-master/HOL4/src/integer/testing/
H A Dtcooper.c73 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 Dbash_process.c26 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 Dbash_process.c26 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 Dlocking.cpp202 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 Dtiming.cpp219 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 Dheapsizing.cpp659 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 Dstatistics.cpp670 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 Dschorr_waite.c88 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 DSpanSpaceScript.sml532 (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 DbddTools.sml124 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 DunifyTools.sml46 fun occurs tv ty = mem tv (type_vars ty)
/seL4-l4v-master/HOL4/examples/HolBdd/
H A DPrimitiveBddRules.sml495 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 DDerivedBddRules.sml691 (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 DTYPECHECK_PARSETREE.sml1472 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 DCODEGEN_PARSETREE.sml301 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 DLogging.sml528 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 Dx64_stepLib.sml1088 val tv = boolSyntax.mk_eq (l, v) value
1090 if List.exists (aconv tv) rst
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DDEBUGGER_.sml221 val filterTypeVars = List.filter (fn tv => not TYPEIDCODE.justForEqualityTypes orelse tvEquality tv)
H A DTYPEIDCODE.sml151 SOME (tv, _) => SOME(TypeVar tv)

Completed in 622 milliseconds