/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_SimpleBuffer.sig | 4 val mkBuffer : unit -> {push : string -> unit, read : unit -> string,
|
H A D | HM_SimpleBuffer.sml | 6 fun push s = buf := s :: !buf function 15 {push = push, read = read, reset = reset}
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | traps.S | 56 * 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 D | target_objects.py | 65 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 D | Proof.C | 53 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 D | Solver.C | 133 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 D | Heap.h | 67 Heap(C c) : comp(c) { heap.push(-1); } 77 heap.push(n);
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | Stack.sig | 7 val push : 'item * 'item stack -> 'item stack value
|
H A D | Stack.sml | 15 fun push( x, S ) = Node( x, S ) function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | Stack.sig | 7 val push : 'item * 'item stack -> 'item stack value
|
H A D | Stack.sml | 15 fun push( x, S ) = Node( x, S ) function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | Stack.sig | 7 val push : 'item * 'item stack -> 'item stack value
|
H A D | Stack.sml | 15 fun push( x, S ) = Node( x, S ) function
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | qbuf.sig | 9 val push : 'a base_tokens.base_token locn.located -> 'a qbuf -> unit value
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | save_vec.cpp | 68 Handle SaveVec::push(PolyWord valu) /* Push a PolyWord onto the save vec. */ function in class:SaveVec
|
H A D | run_time.cpp | 67 #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 D | arb.cpp | 356 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 D | reals.cpp | 198 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 D | process_env.cpp | 120 #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 D | head.S | 25 .option push
|
/seL4-l4v-master/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 43 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 D | mlpp | 43 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 D | utf8.scala | 51 def push(x: Int) 63 else if ((c & 0xC0) == 0x80) push(c & 0x3F)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | utf8.scala | 51 def push(x: Int) 63 else if ((c & 0xC0) == 0x80) push(c & 0x3F)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibCanon.sml | 189 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);
|