/seL4-l4v-master/l4v/ |
H A D | run_tests | 8 import os 18 DIR=os.path.dirname(os.path.realpath(__file__)) 21 os.environ["PATH"] += os.pathsep + DIR 24 os.environ["ISABELLE_TIMING_LOG"]="3.0s" 27 if "QUICK_AND_DIRTY" in os.environ: 28 os.environ["AINVS_QUICK_AND_DIRTY"]=1 29 os.environ["REFINE_QUICK_AND_DIRTY"]=1 30 os [all...] |
/seL4-l4v-master/l4v/tools/autocorres/tools/ |
H A D | release.py | 12 import os namespace 38 os.makedirs(path) 50 for root, dirnames, filenames in os.walk(base_path): 52 results.append(os.path.join(root, filename)) 74 base_dir = os.path.split(pattern)[0] 75 g = glob.glob(os.path.join(base, pattern)) 90 manifest_dest = os.path.join(output_dir, target) 91 os.mkdir(manifest_dest) 92 dir_src = os.path.join(args.repository, manifest_base) 95 mkdir_p(os [all...] |
/seL4-l4v-master/l4v/misc/filemerge/ |
H A D | unicode.py | 18 import os namespace 22 sys.path.append(os.path.join(os.path.dirname(__file__), '../pysymbols')) 24 translator = isasymbols.make_translator(os.path.join(os.path.dirname(__file__),
|
H A D | xsymbol.py | 17 import os namespace 21 sys.path.append(os.path.join(os.path.dirname(__file__), '../pysymbols')) 23 translator = isasymbols.make_translator(os.path.join(os.path.dirname(__file__),
|
/seL4-l4v-master/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-master/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-master/l4v/spec/cspec/ |
H A D | mk_umm_types.py | 15 import os namespace 45 if "ISABELLE_PROCESS" not in os.environ or "ISABELLE_TOOL" not in os.environ: 67 "input": os.path.abspath(args.input), 68 "output": os.path.abspath(args.output), 70 with open(os.path.join(tmp_dir, "UmmTypesFile.thy"), "w") as f: 72 with open(os.path.join(tmp_dir, "ROOT"), "w") as f: 84 os.environ["ISABELLE_TOOL"], "build", "-c"] 85 + interleave("-d", [os.path.abspath(x) for x in args.root])
|
/seL4-l4v-master/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-master/HOL4/src/holyhammer/ |
H A D | hhExportSexpr.sml | 30 fun os oc s = TextIO.output (oc,s) function 37 | a :: m => (f oc a; os oc sep; oiter_aux oc sep f m) 103 if is_vartype ty then os oc (sexpr_vartype ty) else 106 then os oc (sexpr_tyop ty) 107 else (os oc "("; os oc (sexpr_tyop ty); 108 os oc " "; oiter oc " " sexpr_type Args; os oc ")") 112 if is_var tm then os oc (sexpr_var tm) 121 then os o [all...] |
H A D | hhExportTh1.sml | 31 if is_vartype ty then os oc (name_vartype ty) else 33 if Thy = "min" andalso Tyop = "bool" then os oc "$o" 36 os oc "("; th1_type oc tya; 37 os oc " > "; th1_type oc tyb; os oc ")" 39 else if null Args then os oc (name_tyop (Thy,Tyop)) 40 else (os oc "("; os oc (name_tyop (Thy,Tyop)); os oc " @ "; 41 oiter oc " @ " th1_type Args; os o [all...] |
H A D | hhExportTf1.sml | 22 if null argl then os oc s else 23 (os oc s; os oc "("; oiter oc "," f_arg argl; os oc ")") 26 if is_vartype ty then os oc (name_vartype ty) else 38 (os oc "("; tf1_utype oc uty; os oc " > "; tf1_utype oc imty; 39 os oc ")") 41 (os oc "(("; oiter oc " * " tf1_utype (butlast l); os o [all...] |
H A D | hhTptp.sml | 51 if is_vartype ty then os oc (tptp_of_vartype ty) else 56 os oc tyops; 58 else (os oc "("; oiter oc "," write_type Args; os oc ")") 63 os oc "s("; write_type oc (type_of tm); os oc ","; 64 os oc (tptp_of_constvar (length argl) rator); 66 else (os oc "("; oiter oc "," write_term argl; os oc ")"); 67 os o [all...] |
H A D | hhExportTf0.sml | 33 if null argl then os oc s else 34 (os oc s; os oc "("; oiter oc "," f_arg argl; os oc ")") 37 if is_vartype ty then os oc (name_vartype ty) else 52 fun f oc x = os oc (name_vartype x ^ ":" ^ dtype) 54 if null tvl then () else (os oc "!["; oiter oc ", " f tvl; os oc "]: ") 60 os oc (namea_v (v,0) ^ ":"); os o [all...] |
H A D | hhExportTh0.sml | 55 (os oc "("; f_oper oc; os oc " @ "; oiter oc " @ " f_arg argl; os oc ")") 58 if is_vartype ty then os oc (name_vartype ty) else 63 ho_fun oc (fn oc_loc => os oc_loc tyops, th0_ty_poly, Args) 73 fun f oc x = os oc (name_vartype x ^ ":" ^ dtype) 75 if null tvl then () else (os oc "!["; oiter oc ", " f tvl; os oc "]: ") 81 os oc (name_v v ^ ":"); os o [all...] |
H A D | hhExportFof.sml | 29 if null argl then os oc s else 30 (os oc s; os oc "("; oiter oc "," f_arg argl; os oc ")") 33 if is_vartype ty then os oc (name_vartype ty) else 47 then os oc (namea_v (v,0)) 48 else os oc (nameplain_cv (v,0)) 52 (os oc s; os oc "["; oiter oc ", " fof_vzero vl; os o [all...] |
/seL4-l4v-master/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-master/l4v/misc/scripts/ |
H A D | gen_isabelle_root.py | 13 import os namespace 53 output_dir = os.path.dirname(options.output) 60 theories += sorted(glob.glob(os.path.join(d, "*.thy"))) 63 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] 93 thy = os.path.relpath(i, output_dir) 94 thy = os [all...] |
H A D | thydeps | 17 import os 25 isabelle_exe = os.path.join(isabelle_dir, 'bin', 'isabelle') 91 relpath = os.path.relpath(f, base) 121 opts.b = [os.path.realpath(d) for d in opts.b] 125 if not os.path.isdir(opts.I): 127 expected_isabelle = os.path.join(opts.I, 'bin', 'isabelle') 128 if not os.path.exists(expected_isabelle): 135 theory = os.path.relpath(theory, opts.b[0])
|
/seL4-l4v-master/l4v/tools/haskell-translator/ |
H A D | pars_skl.py | 13 import os namespace 14 import os.path namespace 18 dir = os.environ['L4CAP'] 19 dir = os.path.join(dir, 'src') 20 return lambda x: os.path.join(dir, x) 40 output_tmp = os.path.join(os.path.dirname(output), 'pars_skel.tmp') 45 os.path.basename(input)) 101 if not os.path.exists(output_tmp): 105 if os [all...] |
/seL4-l4v-master/l4v/misc/filemerge/faster/ |
H A D | make_tables.py | 10 import os namespace 13 MY_DIR = os.path.dirname(os.path.abspath(__file__)) 15 sys.path.append(os.path.join(MY_DIR, '../../../internal/misc/pysymbols')) 25 with open(os.path.join(MY_DIR, '../../../isabelle/etc/symbols')) as f:
|
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | auto_infea.py | 7 import os, sys, time namespace 20 null_fds = [os.open(os.devnull, os.O_RDWR) for x in xrange(2)] 22 saved_fds = os.dup(1), os.dup(2) 24 os.dup2(null_fds[0], 1) 25 os.dup2(null_fds[1], 2) 33 os.dup2(save_fds[0], 1) 34 os [all...] |
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex.sml | 224 (*val os = Portable.std_out*) 225 fun output_holtex_def_internal (definetype,id,cs) os = 227 val _ = Portable.output (os, definetype); 228 val _ = Portable.output (os, id); 229 val _ = Portable.output (os, "}{"); 230 val _ = Portable.output (os, cs); 231 val _ = Portable.output (os, "}\n"); 239 fun output_holtex_def command definetype os (id, 254 output_holtex_def_internal (definetype,id,cs) os 263 fun process_type_defs os 548 val os = Portable.open_out (basename ^ ".tde") value 551 val os = Portable.open_out (basename ^ ".tid") value [all...] |
/seL4-l4v-master/HOL4/src/opentheory/reader/ |
H A D | OpenTheoryReader.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-master/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-master/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')
|