/seL4-l4v-10.1.1/l4v/ |
H A D | run_tests | 13 import os namespace 21 DIR=os.path.dirname(os.path.realpath(__file__)) 24 os.environ["PATH"] += os.pathsep + DIR 27 if not os.environ.has_key("L4V_ARCH"): 28 os.environ["L4V_ARCH"] = L4V_ARCH_DEFAULT 30 L4V_ARCH=os.environ["L4V_ARCH"] 36 os.environ["L4V_ARCH_IS_ARM"]= L4V_ARCH 46 os [all...] |
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/ |
H A D | release.py | 16 import os namespace 39 os.makedirs(path) 50 for root, dirnames, filenames in os.walk(base_path): 52 results.append(os.path.join(root, filename)) 73 base_dir = os.path.split(pattern)[0] 74 g = glob.glob(os.path.join(base, pattern)) 88 manifest_dest = os.path.join(output_dir, target) 89 os.mkdir(manifest_dest) 90 dir_src = os.path.join(args.repository, manifest_base) 93 mkdir_p(os [all...] |
/seL4-l4v-10.1.1/l4v/misc/filemerge/ |
H A D | unicode.py | 21 import os, sys namespace 24 sys.path.append(os.path.join(os.path.dirname(__file__), '../pysymbols')) 27 translator = isasymbols.make_translator(os.path.join(os.path.dirname(__file__),
|
H A D | xsymbol.py | 21 import os, sys namespace 24 sys.path.append(os.path.join(os.path.dirname(__file__), '../pysymbols')) 27 translator = isasymbols.make_translator(os.path.join(os.path.dirname(__file__),
|
/seL4-l4v-10.1.1/isabelle/Admin/Mercurial/ |
H A D | hgwebdir.cgi | 26 import os namespace 27 os.environ["HGENCODING"] = "UTF-8" 28 os.environ["HGRCPATH"] = "/home/isabelle-repository/repos/hgrc"
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Mercurial/ |
H A D | hgwebdir.cgi | 26 import os namespace 27 os.environ["HGENCODING"] = "UTF-8" 28 os.environ["HGRCPATH"] = "/home/isabelle-repository/repos/hgrc"
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhTptp.sml | 71 fun os oc s = TextIO.output (oc,s) function 76 | a :: m => (f oc a; os oc sep; oiter_aux oc sep f m) 81 if is_vartype ty then os oc (tptp_of_vartype ty) 87 os oc tyops; 89 else (os oc "("; oiter oc "," write_type Args; os oc ")") 96 os oc "s("; write_type oc (type_of tm); os oc ","; 97 os oc (tptp_of_constvar (length argl) rator); 99 else (os o [all...] |
H A D | hhWriter.sml | 149 fun os oc s = output (oc,s) function 164 then os oc (dfind_err "tyvar" ty (!(#tyvar_names state))) 168 if null Args then os oc s else 170 then (os oc "("; oty state oc (hd Args); os oc " > "; 171 oty state oc (hd (tl Args)); os oc ")") 172 else (os oc ("(" ^ s ^ " "); 173 oiter oc " " (oty state oc) Args; os oc ")") 192 if is_var tm then os oc (dfind_err "var" tm (!(#var_names state))) 201 then os o [all...] |
/seL4-l4v-10.1.1/l4v/spec/cspec/ |
H A D | mk_umm_types.py | 19 import os namespace 46 if "ISABELLE_PROCESS" not in os.environ or "ISABELLE_TOOL" not in os.environ: 68 "input": os.path.abspath(args.input), 69 "output": os.path.abspath(args.output), 71 with open(os.path.join(tmp_dir, "UmmTypesFile.thy"), "w") as f: 73 with open(os.path.join(tmp_dir, "ROOT"), "w") as f: 85 os.environ["ISABELLE_TOOL"], "build", "-c"] 86 + interleave("-d", [os.path.abspath(x) for x in args.root])
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | config.sub | 122 os=-$maybe_os 126 os=-linux-android 132 then os=`echo $1 | sed 's/.*-/-/'` 133 else os=; fi 141 case $os in 142 -sun*os*) 152 os= 156 os=-cnk 159 os= 165 os [all...] |
H A D | generate-ios-source-and-headers.py | 5 import os namespace 64 if not os.path.exists(dst_dir): 65 os.makedirs(dst_dir) 70 split_name = os.path.splitext(filename) 73 with open(os.path.join(src_dir, filename)) as in_file: 74 with open(os.path.join(dst_dir, out_filename), 'w') as out_file: 86 for root, dirs, files in os.walk(src_dir, followlinks=True): 87 relroot = os.path.relpath(root,src_dir) 100 outroot = os.path.join(dest_dir, relroot) 124 if not os [all...] |
H A D | generate-osx-source-and-headers.py | 4 import os namespace 58 if not os.path.exists(dst_dir): 59 os.makedirs(dst_dir) 64 split_name = os.path.splitext(filename) 67 with open(os.path.join(src_dir, filename)) as in_file: 68 with open(os.path.join(dst_dir, out_filename), 'w') as out_file: 80 for root, dirs, files in os.walk(src_dir, followlinks=True): 81 relroot = os.path.relpath(root,src_dir) 94 outroot = os.path.join(dest_dir, relroot) 117 if not os [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | config.sub | 122 os=-$maybe_os 126 os=-linux-android 132 then os=`echo $1 | sed 's/.*-/-/'` 133 else os=; fi 141 case $os in 142 -sun*os*) 152 os= 156 os=-cnk 159 os= 165 os [all...] |
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_write.ml | 42 let os = output_string;; var 46 | h :: t -> fn oc h; os oc sep; oiter oc fn sep t;; 146 0 -> os oc (Hashtbl.find ts ty) 149 os oc "("; oty_mono ts 0 oc t1; os oc " > "; oty_mono ts 0 oc t2; os oc ")" 152 os oc "("; oiter oc (oty_mono ts (order - 1)) " > " args; os oc " > "; 153 oty_mono ts (order - 1) oc res; os oc ")" 154 else os o [all...] |
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Database.sml | 16 fun writeInt32 os i = 21 (BinIO.output1 (os, w32tow8 w); 22 BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w8))); 23 BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w16))); 24 BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w24)))) 39 fun writeString os s = 40 (writeInt32 os (String.size s); 41 BinIO.output (os, Byte.stringToBytes s)); 48 fun writeList write os l = 51 BinIO.output1 (os, 168 let val os = BinIO.openOut filename in value [all...] |
/seL4-l4v-10.1.1/l4v/misc/scripts/ |
H A D | gen_isabelle_root.py | 17 import os namespace 54 output_dir = os.path.dirname(options.output) 61 theories += sorted(glob.glob(os.path.join(d, "*.thy"))) 64 session_name = os.path.splitext(os.path.basename(options.output))[0] 66 return os.path.splitext(os.path.relpath(file, os.path.dirname(options.output)))[0] 89 thy = os.path.relpath(i, output_dir) 90 thy = os [all...] |
H A D | thydeps | 23 import os 31 isabelle_exe = os.path.join(isabelle_dir, 'bin', 'isabelle') 97 relpath = os.path.relpath(f, base) 127 opts.b = [os.path.realpath(d) for d in opts.b] 131 if not os.path.isdir(opts.I): 133 expected_isabelle = os.path.join(opts.I, 'bin', 'isabelle') 134 if not os.path.exists(expected_isabelle): 141 theory = os.path.relpath(theory, opts.b[0])
|
/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | pars_skl.py | 17 import os namespace 18 import os.path namespace 22 dir = os.environ['L4CAP'] 23 dir = os.path.join(dir, 'src') 24 return lambda x: os.path.join(dir, x) 44 output_tmp = os.path.join(os.path.dirname(output), 'pars_skel.tmp') 49 os.path.basename(input)) 105 if not os.path.exists(output_tmp): 109 if os [all...] |
/seL4-l4v-10.1.1/l4v/misc/filemerge/faster/ |
H A D | make_tables.py | 13 import argparse, os, sys namespace 15 MY_DIR = os.path.dirname(os.path.abspath(__file__)) 17 sys.path.append(os.path.join(MY_DIR, '../../../internal/misc/pysymbols')) 27 with open(os.path.join(MY_DIR, '../../../isabelle/etc/symbols')) as f:
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | auto_infea.py | 10 import os, sys, time namespace 23 null_fds = [os.open(os.devnull, os.O_RDWR) for x in xrange(2)] 25 saved_fds = os.dup(1), os.dup(2) 27 os.dup2(null_fds[0], 1) 28 os.dup2(null_fds[1], 2) 36 os.dup2(save_fds[0], 1) 37 os [all...] |
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | holindex.sml | 218 (*val os = Portable.std_out*) 219 fun output_holtex_def_internal (definetype,id,cs) os = 221 val _ = Portable.output (os, definetype); 222 val _ = Portable.output (os, id); 223 val _ = Portable.output (os, "}{"); 224 val _ = Portable.output (os, cs); 225 val _ = Portable.output (os, "}\n"); 233 fun output_holtex_def command definetype os (id, 245 output_holtex_def_internal (definetype,id,cs) os 254 fun process_type_defs os 527 val os = Portable.open_out (basename ^ ".tde") value 530 val os = Portable.open_out (basename ^ ".tid") value [all...] |
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
H A D | Opentheory.sml | 158 fun f "absTerm"(st as {stack=OTerm b::OVar v::os,...}) = st_(OTerm(mk_abs(v,b))::os,st) 159 | f "absThm" (st as {stack=OThm th::OVar v::os,...}) = (st_(OThm(ABS v th)::os,st) 161 | f "appTerm"(st as {stack=OTerm x::OTerm f::os,...})= st_(OTerm(mk_comb(f,x))::os,st) 162 | f "appThm" (st as {stack=OThm xy::OThm fg::os,...})= let 167 in st_(OThm(TRANS fxgx gxgy)::os,st) end 168 | f "assume" (st as {stack=OTerm t::os,...}) = st_(OThm(ASSUME t)::os,s [all...] |
/seL4-l4v-10.1.1/HOL4/tools/quote-filter/ |
H A D | mlton-quote-filter.sml | 12 fun noninteractive (is,os) = let 15 (fn () => slave(input, os) (newstate os)) 41 val os = openOut ofile value 48 noninteractive (is,os)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | decompile.py | 31 import os namespace 48 elf = os.path.abspath(args.filename) 49 output_file = os.path.abspath(args.filename + '_output.txt') 58 decompiler_dir = os.path.dirname(sys.argv[0]) 60 os.chdir(decompiler_dir) 69 outp = os.path.abspath('hol_output.txt')
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | platform.scala | 17 val is_linux = System.getProperty("os.name", "") == "Linux" 18 val is_macos = System.getProperty("os.name", "") == "Mac OS X" 19 val is_windows = System.getProperty("os.name", "").startsWith("Windows") 37 System.getProperty("os.arch", "") match { 44 val os = 45 System.getProperty("os.name", "") match { 52 arch + "-" + os
|