Searched refs:push (Results 1 - 25 of 137) sorted by relevance

123456

/seL4-l4v-master/HOL4/tools/Holmake/
H A DHM_SimpleBuffer.sig4 val mkBuffer : unit -> {push : string -> unit, read : unit -> string,
H A DHM_SimpleBuffer.sml6 fun push s = buf := s :: !buf function
15 {push = push, read = read, reset = reset}
/seL4-l4v-master/seL4/src/arch/x86/64/
H A Dtraps.S56 * register we want to push in the case of the fastsyscall trap. See the
71 * FaultIP, and RSP) and are ready to push Error.
104 push %r11; \
107 push %r15; \
108 push %r9; \
109 push %r8; \
110 push %r10; \
111 push %rdx; \
112 push %r14; \
113 push
[all...]
/seL4-l4v-master/graph-refine/
H A Dtarget_objects.py65 def depth_tracer (s, push):
66 if push != 0:
67 trace_depth[0] += push
71 def default_tracer (s, push):
76 def trace (s, push = 0):
77 tracer[0](str (s), push)
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DProof.C53 files.push(name);
72 c2fp.push(0); // dummy argument (placeholder for clause ID 0 which does not exist)
80 c2fp.push(0);
95 c2fp.push(fp.tell());
114 chain_id.push(abs(start)); //HA: the abs
121 chain_id .push(abs(next)); //HA: abs
122 if (next>=0) chain_var.push(x << 1);
123 else chain_var.push((x << 1) | 1); // HA: adding sign info to pivots
129 chain_id .push(abs(next)); //HA: abs
130 chain_var.push(inde
[all...]
H A DSolver.C133 watches[index(~(*c)[0])].push(c);
134 watches[index(~(*c)[1])].push(c);
135 learnts.push(c);
140 watches[index(~(*c)[0])].push(c);
141 watches[index(~(*c)[1])].push(c);
142 clauses.push(c);
192 watches .push(); // (list for positive literal)
193 watches .push(); // (list for negative literal)
194 reason .push(NULL);
195 sreason .push(tru
[all...]
H A DHeap.h67 Heap(C c) : comp(c) { heap.push(-1); }
77 heap.push(n);
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DStack.sig7 val push : 'item * 'item stack -> 'item stack value
H A DStack.sml15 fun push( x, S ) = Node( x, S ) function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DStack.sig7 val push : 'item * 'item stack -> 'item stack value
H A DStack.sml15 fun push( x, S ) = Node( x, S ) function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DStack.sig7 val push : 'item * 'item stack -> 'item stack value
H A DStack.sml15 fun push( x, S ) = Node( x, S ) function
/seL4-l4v-master/HOL4/src/parse/
H A Dqbuf.sig9 val push : 'a base_tokens.base_token locn.located -> 'a qbuf -> unit value
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dsave_vec.cpp68 Handle SaveVec::push(PolyWord valu) /* Push a PolyWord onto the save vec. */ function in class:SaveVec
H A Drun_time.cpp67 #define SAVE(x) taskData->saveVec.push(x)
105 return taskData->saveVec.push(alloc(taskData, size, flags));
185 location = taskData->saveVec.push(TAGGED(0));
188 Handle file = taskData->saveVec.push(C_string_to_Poly(taskData, fileName));
210 Handle exn = make_exn(taskData, id, taskData->saveVec.push(TAGGED(0)), 0, 0);
336 return taskData->saveVec.push(TAGGED(val));
343 return taskData->saveVec.push(TAGGED(uval));
350 return taskData->saveVec.push(TAGGED(val));
357 return taskData->saveVec.push(TAGGED(uval));
365 return taskData->saveVec.push(TAGGE
[all...]
H A Darb.cpp356 return taskData->saveVec.push(TAGGED(-(POLYSIGNED)r));
358 return taskData->saveVec.push(TAGGED(r));
385 return taskData->saveVec.push(TAGGED(-(POLYSIGNED)r));
387 return taskData->saveVec.push(TAGGED(r));
404 return taskData->saveVec.push(TAGGED(val));
427 if (uval <= MAXTAGGED) return taskData->saveVec.push(TAGGED(uval));
470 return taskData->saveVec.push(TAGGED((POLYSIGNED)val));
475 Handle twoTo16 = taskData->saveVec.push(TAGGED(65536));
483 return taskData->saveVec.push(TAGGED((POLYUNSIGNED)uval));
487 Handle twoTo16 = taskData->saveVec.push(TAGGE
[all...]
H A Dreals.cpp198 return mdTaskData->saveVec.push(v);
226 return mdTaskData->saveVec.push(PolyWord::FromSigned(((POLYSIGNED)argx.i << FLT_SHIFT) + 1));
244 return mdTaskData->saveVec.push(v);
261 Handle pushedArg = taskData->saveVec.push(arg);
452 Handle pushedArg = taskData->saveVec.push(arg);
665 Handle pushedString = taskData->saveVec.push(str);
851 Handle ppStr = mdTaskData->saveVec.push(pStr);
857 return mdTaskData->saveVec.push(result);
867 Handle pushedArg = taskData->saveVec.push(arg);
868 Handle pushedMode = taskData->saveVec.push(mod
[all...]
H A Dprocess_env.cpp120 #define SAVE(x) taskData->saveVec.push(x)
196 Handle pushedCode = taskData->saveVec.push(code);
197 Handle pushedArg = taskData->saveVec.push(arg);
251 result = taskData->saveVec.push(C_string_to_Poly(taskData, errorMsg));
256 result = taskData->saveVec.push(C_string_to_Poly(taskData, buff));
362 result = taskData->saveVec.push(C_string_to_Poly(taskData, ""));
363 else result = taskData->saveVec.push(name);
386 result = taskData->saveVec.push(C_string_to_Poly(taskData, userOptions.programName));
426 Handle pushedArg = taskData->saveVec.push(arg);
436 result = taskData->saveVec.push(C_string_to_Pol
[all...]
/seL4-l4v-master/seL4/src/arch/riscv/
H A Dhead.S25 .option push
/seL4-l4v-master/isabelle/src/Tools/Metis/scripts/
H A Dmlpp43 push @ps, "QUOTE \"$q\"" unless ($q eq "");
46 push @ps, "ANTIQUOTE $q";
54 if ($p =~ /QUOTE \"(.*)\"/) { push @ps, "QUOTE \"$1\\n\""; }
55 else { push @ps, $p; push @ps, "QUOTE \"\\n\""; }
57 else { push @ps, "QUOTE \"\\n\""; }
117 push @quotes, $1;
124 push @quotes, "$line\n";
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/scripts/
H A Dmlpp43 push @ps, "QUOTE \"$q\"" unless ($q eq "");
46 push @ps, "ANTIQUOTE $q";
54 if ($p =~ /QUOTE \"(.*)\"/) { push @ps, "QUOTE \"$1\\n\""; }
55 else { push @ps, $p; push @ps, "QUOTE \"\\n\""; }
57 else { push @ps, "QUOTE \"\\n\""; }
117 push @quotes, $1;
124 push @quotes, "$line\n";
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dutf8.scala51 def push(x: Int)
63 else if ((c & 0xC0) == 0x80) push(c & 0x3F)
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dutf8.scala51 def push(x: Int)
63 else if ((c & 0xC0) == 0x80) push(c & 0x3F)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibCanon.sml189 fun push (Or (p,q)) = distrib (push p) (push q) function
190 | push (And (p,q)) = union (push p) (push q)
191 | push fm = [[fm]];
195 | simpcnf fm = List.filter (non tautologous) (push fm);

Completed in 201 milliseconds

123456