/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | armLib.sml | |
H A D | arm_decoderScript.sml | 583 and cond = if IT = 0w then 0b1110w else (7 >< 4) IT value [all...] |
H A D | arm_parserLib.sml | 1085 (let val cond = condition_to_word4 s value 2027 val cond = condition_to_word4 c value 2029 val cond = if b then value 2055 let val cond = condition_to_word4 c in value [all...] |
H A D | arm_random_testingLib.sml | 857 val cond = mk_word4 value
|
H A D | arm_stepLib.sml | 800 val (cond,instruction) = pairSyntax.dest_pair dec value
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_decoderScript.sml | 583 and cond = if IT = 0w then 0b1110w else (7 >< 4) IT value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | lzConv.sml | 1649 let val {cond,larm,rarm} = dest_cond tm value
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 3906 val cond = imk_comb(i,mk_cond(pred,el 1 vars,el 2 vars)); value 3937 val cond = ``COND:bool -> 'a -> 'a -> 'a`` value
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
H A D | decidable_separationLogicLib.sml | 858 val cond = (list_mk_comb (``hyp_in_precond``, [if turn then T else F, numLib.term_of_int n])); value 869 val cond = (list_mk_comb (``hyp_in_self``, [if turn then T else F, numLib.term_of_int m])); value 912 val cond = if isSome condOpt then valOf condOpt else ``hyp_keep``; value 1460 val cond = (e1 = e1') andalso (e2 = e2') andalso value
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS type
|
H A D | annotatedIR.sml | 24 type cond = exp * rop * exp; type 176 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 211 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 257 let val (cond, ((t_cfg,t_start_node),(f_cfg,f_start_node)), join_node) = break_cj cfg n; value 281 let val (cond, ((p_cf value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS type
|
H A D | annotatedIR.sml | 15 type cond = exp * rop * exp; type 166 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 201 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 240 let val (cond, ((t_cfg,t_start_node),(f_cfg,f_start_node)), join_node) = break_cj cfg n; value 264 let val (cond, ((p_cf value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS type
|
H A D | annotatedIR.sml | 15 type cond = exp * rop * exp; type 166 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 201 val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node), value 240 let val (cond, ((t_cfg,t_start_node),(f_cfg,f_start_node)), join_node) = break_cj cfg n; value 264 let val (cond, ((p_cf value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | basic_leakage_examplesScript.sml | 30 infixr 0 ++ << || THENC ORELSEC ORELSER ##;infix 1 >>;val op ++ = op THEN;val op << = op THENL;val op >> = op THEN1;val op || = op ORELSE;val REVERSE = Tactical.REVERSE;val Simplify = RW_TAC arith_ss;val Suff = PARSE_TAC SUFF_TAC;val Know = PARSE_TAC KNOW_TAC;val Rewr = DISCH_THEN (REWRITE_TAC o wrap);val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);val Cond = DISCH_THEN (fn mp_th => let val cond = fst (dest_imp (concl mp_th)) in KNOW_TAC cond << [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] end);val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); value
|
H A D | borelScript.sml | 45 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | dining_cryptosScript.sml | 56 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | extra_realScript.sml | 51 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | informationScript.sml | 53 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | leakageScript.sml | 54 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | lebesgueScript.sml | 54 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | measureScript.sml | 44 val cond = fst (dest_imp (concl mp_th)) value
|
H A D | probabilityScript.sml | 38 val cond = fst (dest_imp (concl mp_th)) value
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
H A D | arm.sml | 2062 val cond = CurrentCond () value 8100 val cond = BitsN.bits(31,28) w value [all...] |