/seL4-l4v-10.1.1/isabelle/Admin/Linux/ |
H A D | build | 3 cc -static -m32 Isabelle.c -o Isabelle
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Linux/ |
H A D | build | 3 cc -static -m32 Isabelle.c -o Isabelle
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.special/ |
H A D | special.exp | 28 dg-runtest [lsort [glob -nocomplain $srcdir/$subdir/*.cc]] $cxx_options "-O0 -W -Wall" 29 dg-runtest [lsort [glob -nocomplain $srcdir/$subdir/*.cc]] $cxx_options "-O2" 30 dg-runtest [lsort [glob -nocomplain $srcdir/$subdir/*.cc]] $cxx_options "-O3" 31 dg-runtest [lsort [glob -nocomplain $srcdir/$subdir/*.cc]] $cxx_options "-Os"
|
/seL4-l4v-10.1.1/isabelle/Admin/bash_process/ |
H A D | build | 40 cc -Wall -m64 bash_process.c -o "$TARGET/bash_process" 43 cc -Wall -m32 bash_process.c -o "$TARGET/bash_process" 46 cc -Wall bash_process.c -o "$TARGET/bash_process.exe" 49 cc -Wall bash_process.c -o "$TARGET/bash_process"
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/bash_process/ |
H A D | build | 40 cc -Wall -m64 bash_process.c -o "$TARGET/bash_process" 43 cc -Wall -m32 bash_process.c -o "$TARGET/bash_process" 46 cc -Wall bash_process.c -o "$TARGET/bash_process.exe" 49 cc -Wall bash_process.c -o "$TARGET/bash_process"
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | call.exp | 22 set tlist [lsearch -inline -all -not -glob [lsort [glob -nocomplain -- $srcdir/$subdir/*.{c,cc}]] *complex*] 23 set ctlist [lsearch -inline -all -glob [lsort [glob -nocomplain -- $srcdir/$subdir/*.{c,cc}]] *complex*]
|
H A D | huge_struct.c | 45 uint32_t cc; member in struct:BigStruct 149 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd, 308 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd, 336 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd,
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | ibm.sml | 44 2 cc 48 assert G (aa -> next_event(bb)(cc before dd)); 70 VAR cc: boolean; 79 (sat_x1 = 4) & (bb & ((!((!dd) & cc)) & (!dd))): 5 union 6; 80 (sat_x1 = 5) & ((!((!dd) & cc)) & (!dd)): 5 union 6; 81 (sat_x1 = 6) & ((!((!dd) & cc)) & dd): 0; 82 (sat_x1 = 7) & (bb & ((!((!dd) & cc)) & dd)): 0; 83 (sat_x1 = 8) & (aa & (bb & ((!((!dd) & cc)) & (!dd)))): 9 union 10; 84 (sat_x1 = 9) & ((!((!dd) & cc)) & (!dd)): 9 union 10; 90 DEFINE spec_define_0:= (!(((sat_x1 = 6) & ((!((!dd) & cc)) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctlCheck.sml | 40 fun ctlCheck I1 T1 state Ric vm ksname (ic,cc) (nf,ctlf) (apl,apsubs) = 41 let val _ = dbgTools.DEN dpfx "cc"(*DBG*) 42 val _ = profTools.bgt (dpfx^"cc")(*PRF*) 43 val (ic,cc) = 45 then (ic,cc) 74 cc) end 79 val _ = profTools.ent (dpfx^"cc")(*PRF*) 80 val ((tb,resthm,trace),(aic,cc)) = absCheck I1 [(".",#6(valOf(#ks(ic))))] state Ric vm ksname (#abs(ic),cc) (nf,mf) (apl,apsubs) 81 val _ = profTools.bgt (dpfx^"cc")(*PR [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 292 const vec<Lit>& cc = clauses[c2c[resolvents[ii]]]; local 293 int csz = cc.size(); 295 update(ps,index(cc[jj]),r1); 392 vec<Lit> cc; local 393 clauses[c2c[ante]].copyTo(cc); 395 for (int ii=0;ii<cc.size();ii++) { 396 if (lit==index(cc[ii])) continue; // skip lit of the var itself 397 int ci = vars[var(cc[ii])]; 401 for (int ii=0;ii<cc.size()-1;ii++) 436 vec<Lit> cc; local [all...] |
/seL4-l4v-10.1.1/HOL4/examples/pgcl/examples/ |
H A D | verification.sml | 113 `monty_choose : int command = ProbAssign "cc" [1; 2; 3]`; 117 Guards [((\v. ~(v"pc" = 1) /\ ~(v"cc" = 1)), (Assign "ac" (\v. 1))); 118 ((\v. ~(v"pc" = 2) /\ ~(v"cc" = 2)), (Assign "ac" (\v. 2))); 119 ((\v. ~(v"pc" = 3) /\ ~(v"cc" = 3)), (Assign "ac" (\v. 3)))]`; 124 else Assign "cc" (\v. if ~(v"cc" = 1) /\ ~(v"ac" = 1) then 1 125 else if ~(v"cc" = 2) /\ ~(v"ac" = 2) then 2 else 3)`; 139 (wlp (monty_hall switch) (\v. if v"pc" = v"cc" then 1 else 0))``, 149 wp (monty_hall switch) (\v. if v"pc" = v"cc" then 1 else 0) =
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | backgroundLib.sml | 85 val cc = RAND_CONV (REPLACE_CONV (GSYM pairTheory.PAIR)) value 86 val cc = cc THENC REPLACE_CONV pairTheory.PAIR_EQ value 87 val th = cc tm
|
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/proof-tests/ |
H A D | struct2.c | 48 cc(struct word_struct word_struct, unsigned v) { function
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stack_logic.py | 298 cc = get_asm_calling_convention_at_node (node) 299 if not cc: 302 arg_vars = set ([var for arg in cc['args'] 305 callee_saved_set = set (cc['callee_saved']) 330 cc = get_asm_calling_convention (fname) 331 callee_saved_set = set (cc['callee_saved']) 332 ret_set = set ([(nm, typ) for ret in cc['rets'] 442 cc = get_asm_calling_convention_at_node (node) 443 assert cc != None, node.fname 444 args = [arg for arg in cc['arg [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mips.sml | 2786 fun dfn'BC1F (i,cc) = 2790 (not(BitsN.bit(#FCC((!fcsr) : FCSR),BitsN.toNat cc)),i); 2792 fun dfn'BC1FL (i,cc) = 2796 (not(BitsN.bit(#FCC((!fcsr) : FCSR),BitsN.toNat cc)),i); 2798 fun dfn'BC1T (i,cc) = 2801 else ConditionalBranch(BitsN.bit(#FCC((!fcsr) : FCSR),BitsN.toNat cc),i); 2803 fun dfn'BC1TL (i,cc) = 2807 (BitsN.bit(#FCC((!fcsr) : FCSR),BitsN.toNat cc),i); 2809 fun dfn'C_cond_D (fs,(ft,(cnd,cc))) = 2813 val i = BitsN.toNat cc [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/ |
H A D | selftest.sml | 58 ``[["acc"]; ["a"; "cc"]; ["ac"; "c"]; ["a"; "c"; "c"]]``; 62 ``[("","acc"); ("a","cc"); ("ac","c"); ("acc","")]``;
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecScript.sml | 38 \\ Q.PAT_X_ASSUM `!kk. (!m. cc) ==> bb` 49 \\ Q.PAT_X_ASSUM `!k. (!m. cc) ==> bb` MATCH_MP_TAC
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Posix.sml | 420 type cc type 421 val cc : (int * char) list -> cc value 422 val update : cc * (int * char) list -> cc 423 val sub : cc * int -> char 499 cc : V.cc, 509 cc : V.cc, 1469 type cc = string type 1471 fun cc l = function [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | ml_bind.sml | 50 structure cc = CommonControls structure
|
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | churchDBScript.sml | 97 Q_TAC (NEW_TAC "cc") `{"v"; "c"; "a"; aa} ��� FV v ��� FV c ��� FV a` THEN 100 LAM cc (LAM aa (VAR cc @@ [VAR cc/"c"]([VAR aa/"a"](ciDB M)) 101 @@ [VAR cc/"c"]([VAR aa/"a"](ciDB N))))) ��� 103 LAM cc (LAM aa ([VAR cc/"c"]([VAR aa/"a"] (ciDB M))))) ��� 105 LAM cc (LAM aa ([VAR cc/"c"]([VAR aa/"a"] (ciDB N)))))` 119 Q_TAC (NEW_TAC "cc") `{" [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sml | 97 fun g (GUARD_COMPARE_LESS false) = ("cc","cs") 127 (* carry *) if tm = ``aS1 psrC`` then ("cs","cc") else
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/ |
H A D | Makefile.am | 74 libffi.call/cls_7_1_byte.c libffi.call/unwindtest.cc \ 75 libffi.call/unwindtest_ffi_call.cc \
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/ |
H A D | mips_stepLib.sml | 374 val BC1F = jEV ``dfn'BC1F (imm, cc)`` 375 val BC1FL = jEV ``dfn'BC1FL (imm, cc)`` 376 val BC1T = jEV ``dfn'BC1T (imm, cc)`` 377 val BC1TL = jEV ``dfn'BC1TL (imm, cc)`` 605 val C_cond_D = fpEV ``dfn'C_cond_D (fs, ft, cnd, cc)`` 606 val C_cond_S = fpEV ``dfn'C_cond_S (fs, ft, cnd, cc)`` 638 val MOVF = fpEV ``dfn'MOVF (rd, fs, cc)`` 639 val MOVF_D = fpEV ``dfn'MOVF_D (fd, fs, cc)`` 640 val MOVF_S = fpEV ``dfn'MOVF_S (fd, fs, cc)`` 641 val MOVT = fpEV ``dfn'MOVT (rd, fs, cc)`` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | IRSyntax.sml | 31 datatype rop = eq | ne | ge | le | gt | lt | al | nv | cc | ls | hi | cs 83 | convert_rop (cc) = Term(`CC:COND`) 283 | to_rop Assem.CC = cc 433 | print_rop (cc) = "<+"
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | IRSyntax.sml | 31 datatype rop = eq | ne | ge | le | gt | lt | al | nv | cc | ls | hi | cs 83 | convert_rop (cc) = Term(`CC:COND`) 275 | to_rop Assem.CC = cc 425 | print_rop (cc) = "<+"
|