/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | pflLib.sml | 23 (* IS_SOME (ifn d args) ==> (ifn d args = ifn (SUC d) args) *) 37 fun dest_args [] = raise ERR "dest_args" "not enough args in function application" 43 val (ifn,args) = strip_comb ifn_app 44 val (d,args') = dest_args args 45 val argfrees = free_varsl args 47 list_mk_forall(args, mk_imp(mk_is_some ifn_app, 54 val ifn_some_goal = list_mk_forall(args [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/ |
H A D | check-file.lisp | 23 (t (let ((args (fold-conses-lst (fargs term)))) 25 (quotep (car args)) 26 (quotep (cadr args))) 27 (kwote (cons (unquote (car args)) 28 (unquote (cadr args))))) 34 args)) 36 args))))))) 46 (('defun fn args . rest) 48 ((not (equal args (formals fn wrld)))
|
/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | syscall_header_gen.py | 232 args = parse_args() variable 234 (api, debug) = parse_xml(args.xml) 235 args.xml.close() 237 if (args.kernel_header is not None): 238 generate_kernel_file(args.kernel_header, api, debug) 239 args.kernel_header.close() 241 if (args.libsel4_header is not None): 242 generate_libsel4_file(args.libsel4_header, api + debug) 243 args.libsel4_header.close()
|
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | syscall_header_gen.py | 232 args = parse_args() variable 234 (api, debug) = parse_xml(args.xml) 235 args.xml.close() 237 if (args.kernel_header is not None): 238 generate_kernel_file(args.kernel_header, api, debug) 239 args.kernel_header.close() 241 if (args.libsel4_header is not None): 242 generate_libsel4_file(args.libsel4_header, api + debug) 243 args.libsel4_header.close()
|
/seL4-l4v-10.1.1/seL4/tools/ |
H A D | syscall_header_gen.py | 232 args = parse_args() variable 234 (api, debug) = parse_xml(args.xml) 235 args.xml.close() 237 if (args.kernel_header is not None): 238 generate_kernel_file(args.kernel_header, api, debug) 239 args.kernel_header.close() 241 if (args.libsel4_header is not None): 242 generate_libsel4_file(args.libsel4_header, api + debug) 243 args.libsel4_header.close()
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | huge_struct.c | 158 cls_large_fn(ffi_cif* cif __UNUSED__, void* resp, void** args, void* userdata __UNUSED__) argument 160 uint8_t ui8_1 = *(uint8_t*)args[0]; 161 int8_t si8_1 = *(int8_t*)args[1]; 162 uint16_t ui16_1 = *(uint16_t*)args[2]; 163 int16_t si16_1 = *(int16_t*)args[3]; 164 uint32_t ui32_1 = *(uint32_t*)args[4]; 165 int32_t si32_1 = *(int32_t*)args[5]; 166 uint64_t ui64_1 = *(uint64_t*)args[6]; 167 int64_t si64_1 = *(int64_t*)args[7]; 168 float f_1 = *(float*)args[ [all...] |
H A D | cls_ulonglong.c | 12 void** args, void* userdata __UNUSED__) 14 *(unsigned long long *)resp= 0xfffffffffffffffLL ^ *(unsigned long long *)args[0]; 16 printf("%" PRIuLL ": %" PRIuLL "\n",*(unsigned long long *)args[0], 11 cls_ret_ulonglong_fn(ffi_cif* cif __UNUSED__, void* resp, void** args, void* userdata __UNUSED__) argument
|
H A D | float1.c | 27 ffi_type *args[MAX_ARGS]; local 33 args[0] = &ffi_type_float; 38 &ffi_type_double, args) == FFI_OK);
|
H A D | float4.c | 29 ffi_type *args[MAX_ARGS]; local 35 args[0] = &ffi_type_double; 40 &ffi_type_double, args) == FFI_OK);
|
H A D | strlen2_win32.c | 19 ffi_type *args[MAX_ARGS]; local 23 args[0] = &ffi_type_pointer; 28 &ffi_type_sint, args) == FFI_OK);
|
H A D | strlen_win32.c | 19 ffi_type *args[MAX_ARGS]; local 23 args[0] = &ffi_type_pointer; 28 &ffi_type_sint, args) == FFI_OK);
|
H A D | struct3.c | 25 ffi_type *args[MAX_ARGS]; local 42 args[0] = &ts3_type; 47 &ts3_type, args) == FFI_OK);
|
H A D | problem1.c | 30 void stub(ffi_cif* cif __UNUSED__, void* resp, void** args, argument 36 a1 = *(struct my_ffi_struct*)(args[0]); 37 a2 = *(struct my_ffi_struct*)(args[1]); 50 void* args[4]; local 74 args[0] = &g; 75 args[1] = &f; 76 args[2] = NULL; 77 ffi_call(&cif, FFI_FN(callee), &res, args);
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | simpleSexpScript.sml | 106 (dstrip_sexp (SX_CONS sym args) = 108 SX_SYM s => OPTION_MAP (��t. (s, t)) (strip_sxcons args) 161 (ptree_digit (Nd (ntm,_) args) = 164 case args of 175 (ptree_sexpnum (Nd (ntm,_) args) = 178 case args of 192 (ptree_WS (Nd (ntm,_) args) = 195 case args of 201 (ptree_grabWS (Nd (ntm,_) args) = 204 case args o [all...] |
/seL4-l4v-10.1.1/seL4/include/machine/ |
H A D | io.h | 40 #define printf(args...) kprintf(args) 44 #define printf(args...) ((void)(0))
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
H A D | holfoot_command_line.sml | 179 val args = CommandLine.arguments (); value 180 val (unicode, args) = (false, Lib.snd (Lib.pluck (fn x => x = "-nu") args)) 181 handle _ => (true, args); 182 val (yices, args) = (true, Lib.snd (Lib.pluck (fn x => x = "--yices") args)) 183 handle _ => (false, args); 187 if length args = 1 then 189 val spec_t = parse_holfoot_file (hd args); 194 val pos = valOf (Int.fromString (el 1 args)) 237 val args = orgargs; value 268 val args = ((Lib.pluck (fn x => x = "-h") orgargs);print_help full;[]) value 270 val args = ((Lib.pluck (fn x => x = "-hi") args);print_interactive_help();[]) value [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | DatatypeSimps.sml | 37 val args = make_variant_list 0 "f" [arg0] tys; value 39 arg0 :: args 45 val args = make_variant_list m "x" avoid arg_tyL value 46 val b = variant (args @ avoid) (mk_var("f"^Int.toString n, ty)) 48 ((args, b) :: res, n+1, m+(length arg_tyL), b::(args@avoid)) 51 val (args, _, _, _) = foldl (fn (ty, (res, n, m, avoid)) => value 54 (arg0, rev args) 102 val avoid = input_arg :: flatten (List.map (fn (args, b) => (b :: args)) case_arg 444 val (args, _) = strip_abs c_tm value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | termSyntax.sml | 25 val (f', args) = strip_comb t 27 if length args = 2 andalso aconv f f' then (hd args, hd (tl args)) 45 val (f, args) = strip_comb t 47 if aconv f SUB_t andalso length args = 3 then (hd args, 48 hd (tl args), 49 hd (tl (tl args)))
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | windows_specific.cpp | 215 static Handle simpleExecute(TaskData *taskData, Handle args); 216 static Handle openProcessHandle(TaskData *taskData, Handle args, BOOL fIsRead, BOOL fIsText); 217 static Handle openRegistryKey(TaskData *taskData, Handle args, HKEY hkParent); 218 static Handle createRegistryKey(TaskData *taskData, Handle args, HKEY hkParent); 219 static Handle queryRegistryKey(TaskData *taskData, Handle args, HKEY hkParent); 220 static Handle setRegistryKey(TaskData *taskData, Handle args, HKEY hkParent); 221 static Handle deleteRegistryKey(TaskData *taskData, Handle args, HKEY hkParent); 222 static Handle deleteRegistryValue(TaskData *taskData, Handle args, HKEY hkParent); 223 static Handle enumerateRegistry(TaskData *taskData, Handle args, HKEY hkey, BOOL isKey); 305 Handle OS_spec_dispatch_c(TaskData *taskData, Handle args, Handl argument 857 execute(TaskData *taskData, Handle args) argument 969 simpleExecute(TaskData *taskData, Handle args) argument 1034 openProcessHandle(TaskData *taskData, Handle args, BOOL fIsRead, BOOL fIsText) argument 1085 openRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument 1111 createRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument 1148 deleteRegistryKey(TaskData *taskData, Handle args, HKEY hkParent) argument 1164 deleteRegistryValue(TaskData *taskData, Handle args, HKEY hkParent) argument 1180 queryRegistryKey(TaskData *taskData, Handle args, HKEY hkey) argument 1240 setRegistryKey(TaskData *taskData, Handle args, HKEY hkey) argument 1272 enumerateRegistry(TaskData *taskData, Handle args, HKEY hkey, BOOL isKey) argument [all...] |
H A D | unix_specific.cpp | 376 static Handle waitForProcess(TaskData *taskData, Handle args); 380 static Handle getSysConf(TaskData *taskData, Handle args); 381 static Handle getTTYattrs(TaskData *taskData, Handle args); 382 static Handle setTTYattrs(TaskData *taskData, Handle args); 384 static Handle lockCommand(TaskData *taskData, int cmd, Handle args); 395 Handle OS_spec_dispatch_c(TaskData *taskData, Handle args, Handle code) argument 406 unsigned i = get_C_unsigned(taskData, args->Word()); 422 int pid = get_C_long(taskData, DEREFHANDLE(args)->Get(0)); 423 int sig = get_C_long(taskData, DEREFHANDLE(args)->Get(1)); 478 return waitForProcess(taskData, args); 1285 waitForProcess(TaskData *taskData, Handle args) argument 1463 getTTYattrs(TaskData *taskData, Handle args) argument 1503 setTTYattrs(TaskData *taskData, Handle args) argument 1539 lockCommand(TaskData *taskData, int cmd, Handle args) argument 2012 getSysConf(TaskData *taskData, Handle args) argument [all...] |
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/stats/ |
H A D | stats.py | 126 args = parser.parse_args() variable 128 if args.root == None and not args.no_isabelle: 130 if args.root != None: 131 args.root = os.path.abspath(args.root) 133 output = open(args.output, "w") 134 output.write("Processing %s\n\n" % args.output) 140 shutil.copyfile(args.input, os.path.join(tmp_dir, "input.c")) 143 lines_of_code = int(subprocess.check_output(["c_count", args [all...] |
/seL4-l4v-10.1.1/HOL4/tools/set_mtime/ |
H A D | set_mtime.sml | 16 fun process_file_args (qf,df,acc) changefile args = 17 case args of 21 fun process_args (qf0,df0) args = 22 case args of 24 | "-q" :: rest => process_args (true, df0) args 25 | "-d" :: rest => process_args (qf0, true) args 40 val (qf,df,changefile,args) = 42 val t = List.foldl (maxtime (qf,df)) Time.zeroTime args
|
/seL4-l4v-10.1.1/isabelle/Admin/jenkins/build/ |
H A D | ci_build_benchmark.scala | 12 def pre_hook(args: List[String]) = {}
|
H A D | ci_build_makeall.scala | 11 def pre_hook(args: List[String]) = {}
|
H A D | ci_build_makeall_seq.scala | 11 def pre_hook(args: List[String]) = {}
|