Searched refs:count (Results 1 - 25 of 316) sorted by path

1234567891011>>

/seL4-l4v-master/HOL4/Manual/Quick/
H A Dquick.tex298 \hol{Count}{apply} \var{function} & returns the theorem count for a function application \\
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dmisc.tex809 incremented. A total count as well as counts per primitive inference
848 the argument \ml{x} and performs a count of inferences during this
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dproof-tools.tex614 contate e aggiunte da \ml{count\_vars} alla map che si accumula, e la
617 La funzione \ml{count\_vars} ha la seguente implementazione:
H A Dtool.tex450 count of the number of intermediate theorems that are generated (which
1325 inference count.
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dtool.tex450 count of the number of intermediate theorems that are generated (which
1325 inference count.
/seL4-l4v-master/HOL4/examples/ARM/v4/mlton/
H A DevalML.sml389 fun print_state fname state count =
396 TextIO.output(ostrm,"Instuctions Run:" ^ Int.toString count ^ "\n");
528 val count = ref 0; value
533 let val _ = count := !count + 1
536 val _ = printer watches (!count) s ns
577 val _ = print_state "run.out" final_state (!count);
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A DarmLib.sml232 val count = pad 8 o pad0 4 o lower o toHexString value
234 List.app (fn (n,i) => output_code ostrm (count (start + n)) i)
H A Darm_encoderLib.sml1490 val count = StringCvt.padLeft #" " 8 o pad 4 o lower o toHexString
1492 app (fn (n,i) => print (count (start + n) ^ " " ^ i ^ "\n"))
H A Darm_parserLib.sml3095 let val count = bit_count list in value
3113 if count = 1 andalso not narrow_okay then
3144 if count = 1 then
3170 val count = bit_count list value
3198 if count = 1 andalso not narrow_okay then
H A Darm_seq_monadScript.sml807 let count = FST (coprocessors.load_count inst coprocessors.state)
810 (forT 0 (count - 1) readm)
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sig32 count (* max number of cycles, -ve for unbounded *)
H A Demit_eval.sml305 "count leading zeroes"
684 fun arm_run trace prog options count =
688 ptree_arm_run trace (prog, state) count
701 val count = input_number (fn i => ~1 <= i) "Enter number of cycles: " value
703 case time (arm_run (int_to_trace trace) prog options) count
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/
H A Darm_seq_monadScript.sml813 let count = FST (coprocessors.load_count inst coprocessors.state)
816 (forT 0 (count - 1) readm)
H A Darm_stepScript.sml3893 let count = n2w (4 * bit_count registers) in
3894 let address = if add then rn else rn - count in
3897 let address = address + (count - 4w)
4057 let count = 4 * bit_count registers in
4058 let base_address = if add then rn else rn - n2w count in
4064 constT (SOME (align (start_address,4) + n2w (count - 4)))))
4085 let count = 4 * bit_count registers in
4086 let base_address = if add then rn else rn - n2w count in
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DksTools.sml119 (* we do not count any atomic propositions over next state variables since by defn AP's are :state->bool *)
H A DprofTools.sml32 fun prc s = if !prf then print (s^".count = "^(Int.toString(find(!cnt,s)))^"\n") else ()
46 (* timers (also have their own call count and inference count) *)
72 val _ = print ("count = "^(Int.toString(find(!cnt,s)))^"\t")
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/
H A DExtendedSyntaxScript.sml86 | ES_RANGE_REPEAT of esere # count (* r[*i] *)
88 | ES_RANGE_EQ_REPEAT of ebexp # count (* b[= i] *)
89 | ES_RANGE_GOTO_REPEAT of ebexp # count (* b[-> i] *)
H A DSyntacticSugarScript.sml149 `count = NUM of num (* number *)
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A Dhol_defaxiomsScript.sml2183 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count
2184 > down for positive exponents and count up for negative exponents
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dhol_defaxiomsScript.sml2153 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count
2154 > down for positive exponents and count up for negative exponents
/seL4-l4v-master/HOL4/examples/acl2/examples/
H A DtestEncode.sml467 val count_def = Define ` (count (Branch []) = 0n) /\
468 (count (Branch ((x,hd)::tl)) = 1 + count (hd:num rose_tree) + count (Branch tl))`;
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dhol_defaxiomsScript.sml2149 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count
2150 > down for positive exponents and count up for negative exponents
H A DtestACL2encoding.ml23 let val (count,results) = type_tests
26 (count := (!count) + 1 ;
28 int_to_string (!count),failed) :: (!results))
/seL4-l4v-master/HOL4/examples/dev/Fact32/
H A DNOT32.ml38 let val count = !NOT32vInst_count
39 val _ = (NOT32vInst_count := count+1);
40 val inst_name = "NOT32" ^ "_" ^ Int.toString count
H A Dexor32.ml71 let val count = !XOR32vInst_count
72 val _ = (XOR32vInst_count := count+1);
73 val inst_name = "XOR32" ^ "_" ^ Int.toString count

Completed in 167 milliseconds

1234567891011>>