/seL4-l4v-master/isabelle/src/Tools/Graphview/ |
H A D | mutator_dialog.scala | 165 private val inputs: List[(String, Input)] = get_inputs() 182 inputs.map({ 254 val r1 = inputs(2)._2.string 257 inputs(3)._2.bool, 259 inputs(1)._2.bool, 260 inputs(0)._2.bool) 264 ident <- space_explode(',', inputs(2)._2.string) 267 inputs(3)._2.bool, 269 inputs(1)._2.bool, 270 inputs( [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/ |
H A D | mutator_dialog.scala | 165 private val inputs: List[(String, Input)] = get_inputs() 182 inputs.map({ 254 val r1 = inputs(2)._2.string 257 inputs(3)._2.bool, 259 inputs(1)._2.bool, 260 inputs(0)._2.bool) 264 ident <- space_explode(',', inputs(2)._2.string) 267 inputs(3)._2.bool, 269 inputs(1)._2.bool, 270 inputs( [all...] |
/seL4-l4v-master/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 17 val _ = Datatype ` P = Func (string list) (* inputs/outputs *) 82 eval_P c inputs (Func args requires body) (n:num) = 83 if req_holds requires inputs then 85 | NonRec d => SOME [FST (eval_D c inputs d)] 88 SOME (MAP (\v. inputs ' v) args) 90 let (_,env) = eval_B c inputs b in 150 inputs_ok c inputs fp_inputs reqs = 151 (FDOM inputs = FDOM fp_inputs) /\ 152 EVERY (eval_A real_conf inputs) reqs /\ 155 ���fp r r'. (FLOOKUP inputs [all...] |
/seL4-l4v-master/seL4/manual/tools/ |
H A D | gen_invocations.py | 39 def generate_prototype(interface_name, method_name, method_id, inputs, outputs, comment): 50 param_list = syscall_stub_gen.generate_param_list(inputs, outputs) 84 for (interface_name, method_name, method_id, inputs, outputs, _, comment) in methods: 87 method_name, method_id, inputs, outputs, comment)
|
/seL4-l4v-master/HOL4/examples/HolBdd/ |
H A D | MachineTransitionScript.sml | 948 `Moore nextfn ((inputs:num->'a),(states:num->'b)) = 949 !t. states(t+1) = nextfn(inputs t,states t)`; 978 ``Moore nextfn (inputs,states) = 980 (MooreTrans nextfn, (inputs 0,states 0)) 981 (\t. (inputs t, states t))``, 997 [``\(input:'a,state:'b). (input = inputs 0) /\ (state = states 0)``, 1018 `(!inputs states. 1019 B(inputs 0, states 0) /\ Moore nextfn (inputs,states) 1020 ==> !t. P(inputs [all...] |
/seL4-l4v-master/HOL4/examples/acl2/tests/obsolete/ |
H A D | doit.bash | 6 inputs_dir=$tests_dir/inputs
|
H A D | doit.csh | 4 set inputs_dir = $tests_dir/inputs
|
/seL4-l4v-master/HOL4/src/n-bit/interactive_tests/ |
H A D | test_wordppScript.sml | 19 fun run_tests tys expected inputs = let 20 val inputs' = remove expected inputs 21 val tests = List.concat (map (zip tys) (map (zip expected) inputs')) in
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 33 nodeLst inputs; 94 initial inputs actions 103 inputs: label 273 bdd_setvarnum(inputs.size()); 276 for (nodeLst::ite i=inputs.first() ; i.more() ; i++, vnum++) 292 inputs.append( nodeData(inputTag,sdup(id->id),bddtrue) );
|
/seL4-l4v-master/HOL4/examples/acl2/tests/ |
H A D | doit | 6 inputs_dir=$tests_dir/inputs
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_types.sig | 44 rule database and dependency database, extending those given as inputs, and
|
/seL4-l4v-master/graph-refine/ |
H A D | inst_logic.py | 95 for (nm, typ) in l_fun.inputs] 162 (iscs, imems, _) = logic.split_scalar_pairs (functions[fname].inputs)
|
H A D | problem.py | 77 self.entries = [(fun.entry, tag, fun.name, fun.inputs)] 108 args = [(vs[v], typ) for (v, typ) in fun.inputs] 142 renames[tag + '_IN'] = mk (fun.inputs, args) 370 for (n, tag, fname, inputs) in self.entries: 372 '%d' % len (inputs)] 373 for (nm, typ) in inputs: 494 (n, inputs) = syntax.parse_list (syntax.parse_lval, bits, 4) 497 p.entries.append ((en, tag, fname, inputs)) 732 inp_lvs = [(vs[v], typ) for (v, typ) in fun.inputs]
|
H A D | syntax.py | 105 of the list. For instance, the classic 'XOR' function with inputs x, y and 791 def __init__ (self, name, inputs, outputs): 793 self.inputs = inputs 802 return hash (tuple ([self.name, tuple (self.inputs), 826 xs = ['Function', self.name, str (len (self.inputs))] 827 for (nm, typ) in self.inputs: 1137 # Function <name> <inputs> <outputs> 1141 (n, inputs) = parse_list (parse_arg, bits, 2) 1143 current_function = Function (fname, inputs, output [all...] |
H A D | pseudo_compile.py | 339 function.inputs = expand_lval_list (replaces, function.inputs) 462 f.inputs = [(renames.get (v, v), t) for (v, t) in f.inputs]
|
H A D | debug.py | 31 for (entry, tag, _, inputs) in p.entries: 35 diff = set (var_deps[entry]) - set (inputs) 603 as_args = functions[p['ASM']].inputs 604 c_args = functions[p['C']].inputs
|
H A D | trace_refute.py | 223 inps = functions[fname].inputs 323 for (entry, tag, _, inputs) in p.entries: 326 for assn in f (inputs):
|
H A D | stack_logic.py | 272 (inputs, outputs, _) = rep.funcs[(n, vc)] 275 inp_sp = solver.smt_expr (sp, inputs, rep.solv) 922 (nm, typ) = functions[fname].inputs[i] 985 (var_c_args, c_imem, glob_c_args) = split_scalar_pairs (c_fun.inputs) 1050 arg_input_map = dict (azip (fun.inputs, node.args)) 1114 in enumerate (functions[f].inputs) 1129 (var_c_args, c_imem, glob_c_args) = split_scalar_pairs (c_fun.inputs)
|
H A D | rep_graph.py | 695 for ((x, typ), arg) in azip (fun.inputs, node.args)]) 697 for (x, typ) in reversed (fun.inputs): 788 def add_func (self, name, inputs, outputs, success, n_vc): 790 self.funcs[n_vc] = (inputs, outputs, success)
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SolverSpec.sml | 23 val (x, inputs) = pre goal 27 val _ = Library.write_strings_to_file infile inputs
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | semi_automatonScript.sml | 39 (* the powerset of a set of propositional varibales as inputs *) 45 I: 'input set; (*set of inputs *)
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | DatatypeSimps.sig | 40 that fires if all inputs give the same result.
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | count.ml | 140 % Similar to COUNT_CORRECT2 but weaker assumptions on inputs %
|
/seL4-l4v-master/HOL4/examples/computability/register/ |
H A D | rmRecursiveFuncsScript.sml | 171 (* Assumption: ((guard, count), (accumulator, inputs))*) 204 (* Assumption: ((guard, count), (accumulator, inputs))*)
|
/seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
H A D | smlParallel.sml | 140 Smart allocation of inputs to waiting threads 152 (* update process inputs *)
|