Searched refs:os (Results 1 - 25 of 74) sorted by relevance

123

/seL4-l4v-master/l4v/
H A Drun_tests8 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 Drelease.py12 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 Dunicode.py18 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 Dxsymbol.py17 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 Dhgwebdir.cgi26 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 Dhgwebdir.cgi26 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 Dmk_umm_types.py15 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 Dconfig.sub122 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 DhhExportSexpr.sml30 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 DhhExportTh1.sml31 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 DhhExportTf1.sml22 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 DhhTptp.sml51 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 DhhExportTf0.sml33 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 DhhExportTh0.sml55 (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 DhhExportFof.sml29 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 DDatabase.sml16 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 Dgen_isabelle_root.py13 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 Dthydeps17 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 Dpars_skl.py13 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 Dmake_tables.py10 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 Dauto_infea.py7 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 Dholindex.sml224 (*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 DOpenTheoryReader.sml158 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 Dmlton-quote-filter.sml12 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 Ddecompile.py31 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')

Completed in 378 milliseconds

123