/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/failing/ |
H A D | dirty_frees.c | 19 int f2(int, int); 21 return f2(l2_f1, l2_f2); 23 int f2(int l2_f1, int l2_f2) { function
|
/seL4-l4v-10.1.1/graph-refine/example/ |
H A D | target.py | 32 f2 = 'mc_' + f[2:] 34 f2 = f + '_refine' 35 if f2 in functions: 36 pair = logic.mk_pairing (functions, f, f2) 38 pairings[f2] = [pair]
|
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/ |
H A D | target.py | 32 f2 = 'mc_' + f[2:] 34 f2 = f + '_impl' 35 if f2 in functions: 36 pair = logic.mk_pairing (functions, f, f2) 38 pairings[f2] = [pair]
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | jiraver150.c | 16 int f2(unsigned z) function
|
H A D | jiraver456.c | 26 struct div_t f2(unsigned n, unsigned d) function
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | ctl_starScript.sml | 42 | CTL_STAR_AND of ctl_star # ctl_star (* f1 \wedge f2 *) 44 | CTL_STAR_PSUNTIL of ctl_star # ctl_star (* f1 U f2 *) 46 | CTL_STAR_SUNTIL of ctl_star # ctl_star (* f1 U f2 *) 63 [`P`,`\(f1,f2). P f1 /\ P f2`] 71 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_AND(f1,f2)) p = CTL_STAR_SEM_PATH_TIME t M f1 p /\ CTL_STAR_SEM_PATH_TIME t M f2 p) /\ 76 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_SUNTIL(f1,f2)) p = (?k. k >= t /\ CTL_STAR_SEM_PATH_TIME k M f2 p /\ 78 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PSUNTIL(f1,f2)) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | ltlScript.sml | 21 /\ (MODELS w (DISJ f1 f2) = (MODELS w f1) \/ (MODELS w f2)) 22 /\ (MODELS w (CONJ f1 f2) = (MODELS w f1) /\ (MODELS w f2)) 24 /\ (MODELS w (U f1 f2) = 25 ?n. (MODELS (suff w n) f2) /\ !i. (i < n) ==> (MODELS (suff w i) f1)) 26 /\ (MODELS w (R f1 f2) = 27 !n. (MODELS (suff w n) f2) \/ ?i. (i < n) /\ (MODELS (suff w i) f1))`; 31 ``!w f1 f2. (!n. (MODELS (suff w n) f2) \/ [all...] |
H A D | ltl2waaScript.sml | 14 `finalForms f = {U f1 f2 | (U f1 f2) ��� tempSubForms f}`; 23 /\ (trans �� (CONJ f1 f2) = d_conj (trans �� f1) (trans �� f2)) 24 /\ (trans �� (DISJ f1 f2) = (trans �� f1) ��� (trans �� f2)) 26 /\ (trans �� (U f1 f2) = (trans �� f2) ��� (d_conj (trans �� f1) {(��,{U f1 f2})})) 27 /\ (trans �� (R f1 f2) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/decompiler/ |
H A D | mips_decomp_demoScript.sml | 21 `abs.d $f2, $f2 22 sqrt.d $f1, $f2 23 neg.d $f2, $f1 24 mov.d $f1, $f2 25 add.d $f3, $f1, $f2 26 sub.d $f1, $f2, $f3 28 div.d $f2, $f2, $f1 29 madd.d $f2, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | ACFScript.sml | 15 `sc (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`; 19 `cj f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 23 `tr (x:'a) = if f1 x then x else tr (f2 x)`; 33 ``!f f1 f2. 34 (!x:'a. f x = if f1(x) then x else f(f2 x)) 35 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f2 x) x)) 36 ==> (f:'a->'a = tr f1 f2)``, 49 ``!f f1 f2 f [all...] |
H A D | cpsSyntax.sml | 13 fun mk_seq(f1,f2) = 15 val (d2,r2) = dom_rng (type_of f2) 17 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]seq_tm,[f1,f2]) 21 fun mk_par(f1,f2) = 23 val (d2,r2) = dom_rng (type_of f2) 25 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]par_tm,[f1,f2]) 29 fun mk_ite(f1,f2,f3) = 31 val (_,r2) = dom_rng (type_of f2) 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/ |
H A D | ACL2BisimScript.sml | 55 (VARS (AND f1 f2) = VARS f1 UNION VARS f2) 57 (VARS (OR f1 f2) = VARS f1 UNION VARS f2) 65 (VARS (UNTIL f1 f2) = VARS f1 UNION VARS f2) 67 (VARS (WEAK_UNTIL f1 f2) = VARS f1 UNION VARS f2)`;
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | struct7.c | 12 float f2; member in struct:__anon63 19 ts.f2 += 1; 55 ts7_arg.f2 = 55.5f; 59 printf ("%g\n", ts7_arg.f2); 65 printf ("%g\n", ts7_result->f2); 69 CHECK(ts7_result->f2 == 55.5f + 1);
|
H A D | struct8.c | 12 float f2; member in struct:__anon64 20 ts.f2 += 1; 58 ts8_arg.f2 = 55.5f; 63 printf ("%g\n", ts8_arg.f2); 70 printf ("%g\n", ts8_result->f2); 75 CHECK(ts8_result->f2 == 55.5f + 1);
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ExtendedSyntaxScript.sml | 103 | EF_AND of efl # efl (* f1 \wedge f2 *) 107 | EF_U of efl # efl (* [f1 U f2] *) 112 | EF_OR of efl # efl (* f1 \vee f2 *) 113 | EF_IMP of efl # efl (* f1 \rightarrow f2 *) 114 | EF_IFF of efl # efl (* f1 \leftrightarrow f2 *) 118 | EF_W of efl # efl (* [f1 W f2] *) 124 | EF_STRONG_UNTIL of efl # efl (* [f1 until! f2] *) 125 | EF_WEAK_UNTIL of efl # efl (* [f1 until f2] *) 126 | EF_STRONG_UNTIL_INC of efl # efl (* [f1 until!_ f2] *) 127 | EF_WEAK_UNTIL_INC of efl # efl (* [f1 until_ f2] *) [all...] |
H A D | SyntacticSugarScript.sml | 229 * Formula disjunction: f1 \/ f2 233 `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`; 236 * Formula implication: f1 --> f2 240 `F_IMPLIES(f1,f2) = F_OR(F_NOT f1, f2)`; 243 * Formula implication: f1 --> f2 251 * Formula equivalence: f1 <--> f2 255 `F_IFF(f1,f2) = F_AND(F_IMPLIES(f1, f2), F_IMPLIE [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | rltl_to_ltlScript.sml | 39 (RLTL_TO_LTL a r (RLTL_AND(f1,f2)) = 40 LTL_AND(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) 45 (RLTL_TO_LTL a r (RLTL_SUNTIL(f1, f2))= 46 LTL_SUNTIL(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) 56 ``!a r f1 f2. 57 (RLTL_TO_LTL a r (RLTL_OR(f1,f2)) = LTL_OR(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\ 58 (RLTL_TO_LTL a r (RLTL_IMPL(f1,f2)) = LTL_IMPL(RLTL_TO_LTL r a f1, RLTL_TO_LTL a r f2)) /\ 59 (RLTL_TO_LTL a r (RLTL_BEFORE(f1,f2)) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | SyntacticSugarScript.sml | 209 * Formula disjunction: f1 \/ f2 213 `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`; 216 * Formula implication: f1 --> f2 220 `F_IMPLIES(f1,f2) = F_OR(F_NOT f1, f2)`; 223 * Formula implication: f1 --> f2 231 * Formula equivalence: f1 <--> f2 235 `F_IFF(f1,f2) = F_AND(F_IMPLIES(f1, f2), F_IMPLIE [all...] |
H A D | ExtendedSyntaxScript.sml | 88 | EF_AND of efl # efl (* f1 \wedge f2 *) 90 | EF_U of efl # efl (* [f1 U f2] *) 98 | EF_OR of efl # efl (* f1 \vee f2 *) 99 | EF_IMP of efl # efl (* f1 \rightarrow f2 *) 100 | EF_IFF of efl # efl (* f1 \leftrightarrow f2 *) 104 | EF_W of efl # efl (* [f1 W f2] *) 110 | EF_STRONG_UNTIL of efl # efl (* [f1 until! f2] *) 111 | EF_WEAK_UNTIL of efl # efl (* [f1 until f2] *) 112 | EF_STRONG_UNTIL_INC of efl # efl (* [f1 until!_ f2] *) 113 | EF_WEAK_UNTIL_INC of efl # efl (* [f1 until_ f2] *) [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/ |
H A D | SGAUnicodeMergeA2Script.sml | 13 ``FUNION f1 f2 x <=> f1 x \/ f2 x``);
|
H A D | SGAUnicodeMergeBScript.sml | 18 ``FUNION f1 f2 = f1 ��� f2``, (* UOK *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/examples/ |
H A D | fc_examples.sml | 14 val def2 = Define `f2 x = x * f1 x`; 18 val def3 = Define `f3 x = x + f2 x`; 24 val def5 = Define `f5(x:word32,y) = y + (f4 (x, f2 y, y)) + x`; 29 let a = if (x >= y) then f2 y else x in 48 let c = if (a <= b) then (f2 a) + b else b in
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | cpsSyntax.sml | 13 fun mk_seq(f1,f2) = 15 val (d2,r2) = dom_rng (type_of f2) 17 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]seq_tm,[f1,f2]) 21 fun mk_par(f1,f2) = 23 val (d2,r2) = dom_rng (type_of f2) 25 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]par_tm,[f1,f2]) 29 fun mk_ite(f1,f2,f3) = 31 val (_,r2) = dom_rng (type_of f2) 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | cpsSyntax.sml | 13 fun mk_seq(f1,f2) = 15 val (d2,r2) = dom_rng (type_of f2) 17 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]seq_tm,[f1,f2]) 21 fun mk_par(f1,f2) = 23 val (d2,r2) = dom_rng (type_of f2) 25 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]par_tm,[f1,f2]) 29 fun mk_ite(f1,f2,f3) = 31 val (_,r2) = dom_rng (type_of f2) 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f [all...] |
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDSupportScript.sml | 22 /\ (sum_retrieve _ f2 (INR a2) (_, b2) = f2 a2 b2)`; 26 /\ (prod_retrieve _ f2 (_, a2) (INR b2) = f2 a2 b2)`;
|