/seL4-l4v-master/l4v/tools/c-parser/testfiles/errors/ |
H A D | addrlocal.c | 7 void swap(int *i1, int *i2) function 20 swap(&i, &j);
|
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | ptr_umm.c | 7 int swap(int *i, int *j) function
|
H A D | swap.c | 10 PROC swap(\<acute>p,\<acute>q) 14 void swap(unsigned int *p, unsigned int *q) function 33 swap(a,b); 34 swap(c,a);
|
/seL4-l4v-master/l4v/tools/autocorres/doc/quickstart/ |
H A D | swap.c | 11 void swap(unsigned *a, unsigned *b) function
|
/seL4-l4v-master/l4v/tools/autocorres/tests/examples/ |
H A D | swap.c | 7 void swap(unsigned *a, unsigned *b) function
|
/seL4-l4v-master/HOL4/examples/lambda/other-models/ |
H A D | swapScript.sml | 5 val _ = new_theory "swap" 112 val swap_def = new_specification("swap_def", ["swap"], thm1); 116 ``!t. swap x x t = t``, 123 ``!t. swap x y t = swap y x t``, 131 ``!t. ~(v IN FV t) ==> ([VAR v/u] t = swap v u t)``, 156 ``!t u v. FV (swap u v t) = swapset u v (FV t)``, 168 ``!t x y. size (swap x y t) = size t``, 187 ``!t u v x y. swap u v ([VAR x/y] t) = 188 [VAR (swapstr u v x)/swapstr u v y] (swap [all...] |
/seL4-l4v-master/HOL4/examples/pgcl/src/ |
H A D | posrealTools.sml | 188 fun bubble is_op swap inv tm = 200 else REWR_CONV swap THENC RAND_CONV (bubble is_op swap inv) 203 fun sort is_op swap inv tm = 205 else RAND_CONV (sort is_op swap inv) THENC bubble is_op swap inv) tm; 207 fun permute is_op assoc rid swap inv = 210 THENC sort is_op swap inv; 212 fun permute_conv is_op assoc rid swap inv tm = 213 (if is_op tm then permute is_op assoc rid swap in [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | UTuple.sml | 16 fun swap (x,y) = (y,x) function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | UTuple.sml | 16 fun swap (x,y) = (y,x) function
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | UTuple.sml | 16 fun swap (x,y) = (y,x) function
|
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
H A D | basics.sml | 117 fun swap (x,y) = (y,x) function 131 (subset eq (xs,ys) andalso subset (eq o swap) (ys,xs))
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | L3.sig | 45 val swap : 'a * 'b -> 'b * 'a value
|
H A D | L3.sml | 109 fun swap (n, l) = (l, n) function
|
/seL4-l4v-master/HOL4/examples/fsub/ |
H A D | fsubtypesScript.sml | 17 This theory establishes the type, along with swap functions for the type 158 (* definition of swap *) 160 fswap x y ty = term2fsubty (swap x y (fsubty2term ty)) 165 ``!t. fsubrep t ==> !x y. fsubrep (swap x y t)``, 200 (* define swap over contexts *)
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | cheney_allocScript.sml | 46 ``!i j. bijection (swap i j)``, 468 (apply (swap i j) s = s)``, 584 \\ Q.EXISTS_TAC `b' o swap i' (k (fresh h))` 587 \\ ASM_SIMP_TAC bool_ss [METIS_PROVE [swap_def] ``!i k. swap i k i = k``] 596 \\ `(MAP b' (MAP (swap i' (k (fresh h))) t) = t2::ts)` by 652 \\ `swap i' (k (fresh h)) o swap i' (k (fresh h)) = I` by METIS_TAC [swap_swap] 654 \\ (ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`swap i' (k (fresh h))`,`swap i' (k (fresh h))`]) apply_INSERT 656 \\ `swap [all...] |
H A D | cheney_gcScript.sml | 188 swap i j = \k. if k = i then j else if k = j then i else k`; 191 ``!i:'a j. swap i j o swap i j = I``, 197 ``!i:'a j x. swap i j (swap i j x) = x``, 203 ``!i j k. ~(i = k) /\ ~(j = k) ==> (swap i j k = k)``, 235 (ADDR k (swap j x t) (((x =+ REF j) ((j =+ (DATA (n',n'',d'))) m)) k) = 285 (((x =+ REF j) ((j =+ DATA (n',n'',d')) m) (swap j x a) = DATA (k,k',v)) = 296 (apply (swap j x) (abs((x =+ REF j) ((j =+ m x) m))) = abs m)``, 310 ``!i j s t. (apply (swap [all...] |
/seL4-l4v-master/HOL4/examples/lambda/basics/ |
H A D | nomdatatype.sml | 15 fun list_mk_icomb(f, args) = List.foldl (mk_icomb o swap) f args 70 val union = List.foldl (mk_union o swap) (hd sets) (tl sets) 120 val list_mk_icomb = uncurry (List.foldl (mk_icomb o swap))
|
H A D | binderLib.sml | 458 ("Couldn't prove function with swap over range - \n\ 466 ("Couldn't prove function with swap over range - \n\ 492 ("Couldn't prove function with swap over range - \n\ 504 ("Couldn't prove function with swap over range - \n\
|
/seL4-l4v-master/HOL4/examples/imperative/ |
H A D | necec2010.sml | 290 A useful function on state spaces is the swap command which is defined as: 311 val _ = tprint ("swap is possible with introduction of temporary variable: " ); 388 In the special case where both variables are numbers, an algebraic method can be used to swap the values without the use of a temporary variable. 397 val _ = tprint ("swap is possible for num type without need for temporary variable: " );
|
/seL4-l4v-master/HOL4/examples/AI_TNN/ |
H A D | mleArithData.sml | 157 let val d = dregroup Int.compare (map swap (map_assoc f tml)) in
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_opsScript.sml | 377 val swap = swap_thm i value 378 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 379 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 412 val swap = swap_thm i value 413 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 414 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 445 val swap = swap_thm i value 446 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 447 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 484 val swap value 511 val swap = swap_thm i value 538 val swap = swap_thm i value [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sig | 57 val swap : 'a * 'b -> 'b * 'a value
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sig | 57 val swap : 'a * 'b -> 'b * 'a value
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psBigSteps.sml | 53 dnew (#board_compare game) (map swap (map_snd #board (dlist tree)))
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibRewrite.sml | 188 fun redex_residue lr th = (if lr then I else swap) (dest_unit_eq th); 265 else foldl (fst o rewr_lit neqs o swap) th rest
|