| /seL4-l4v-master/seL4/src/ |
| H A D | assert.c | 16 const char *function)
19 "seL4 called fail at %s:%u in function %s, saying \"%s\"\n",
22 function,
32 const char *function)
34 printf("seL4 failed assertion '%s' at %s:%u in function %s\n",
38 function
12 _fail( const char *s, const char *file, unsigned int line, const char *function) argument
28 _assert_fail( const char *assertion, const char *file, unsigned int line, const char *function) argument
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | KnuthBendixOrder.sig | 11 (* one unary function with weight 0. *)
15 {weight : Term.function -> int,
16 precedence : Term.function * Term.function -> order}
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | KnuthBendixOrder.sig | 11 (* one unary function with weight 0. *)
15 {weight : Term.function -> int,
16 precedence : Term.function * Term.function -> order}
|
| /seL4-l4v-master/seL4/include/machine/ |
| H A D | assembler.h | 19 .type _name, %function ; \
30 .type _name, %function ; \
|
| /seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sig | 8 (* mc_define defines a function and puts the definition on a queue
9 waiting to be compiled, returns function definition and pre *)
12 (* mc_compile fname target: compiles function fname to target code,
16 (* mc_compile_all fname: compiles function fname to all targets *)
23 (* the tactic used for proving function equivalence *)
|
| /seL4-l4v-master/seL4/include/ |
| H A D | assert.h | 18 const char *function
27 const char *function
|
| /seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
| H A D | inner_fncalls.c | 7 /* this proto is for a function not defined in this translation unit */
39 char function(int c) { return c + 1; } function
41 int function2(int x) { return g(function(x)); }
|
| /seL4-l4v-master/seL4/libsel4/include/sel4/ |
| H A D | assert.h | 17 * Hidden function, use the macros seL4_Fail or seL4_Assert.
19 void __assert_fail(const char *str, const char *file, int line, const char *function);
23 * expr as a string plus the file, line and function.
29 * expr as a string plus the file, line and function.
|
| /seL4-l4v-master/HOL4/src/tfl/src/test/ |
| H A D | tfl_examplesScript.sml | 3 fun function s q = Count.apply (bossLib.xDefine s) q; (* tries termination *) function
11 val fact_cond_def = function "fact_cond"
14 val fact_pattern_def = function "fact_pattern"
18 val Ffact_def = function "Ffact" `(Ffact (SUC x) = Ffact x * SUC x)`;
20 val Fib_def = function "Fib"
25 val Ffib_def = function "Ffib" `(Ffib (SUC(SUC x)) = Ffib x + Fib (SUC x))`;
32 val map2_def = function "map2"
37 val Map2_def = function "Map2"
42 val Mmap2_def = function "Mmap2"
47 val sorted_def = function "sorte
[all...] |
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibPortable.sig | 15 (* Timing function applications *)
|
| H A D | mlibPortable.sml | 29 (* Timing function applications a la Mosml.time. *)
|
| /seL4-l4v-master/HOL4/src/monad/ |
| H A D | parmonadsyntax.sig | 11 (* loading this module installs this function as an absyn transformer
|
| /seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sig | 8 This function translates all the functions defined in defs to
12 translate_to_c generates 3 files: filename.h, filename.c and filename-test.c in the directory dirname. The directory name must end with a "/". The file filename.c contains the main function definitions, filename.h the headers.
15 the function main_func. The parameter tests is a list of pairs
16 (f, (arg, res) list). f is the function to be tested, the other list
22 (* This function is intended to generate tests.
|
| /seL4-l4v-master/HOL4/src/hol88/ |
| H A D | hol88Lib.sml | 14 fun HOL88_ERR {function, message} =
16 origin_function = function,
44 of NONE => raise HOL88_ERR {function = "assoc", message = ""}
49 of NONE => raise HOL88_ERR {function = "rev_assoc", message = ""}
72 else raise HOL88_ERR {function = "variant",
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | ord-map-sig.sml | 23 (* Update an item by applying a function to the item already stored.
54 * maps, using the supplied function to define the map on elements that
61 * two input maps, using the supplied function to define the range.
66 (* Apply a function to the entries of the map in map order. *)
70 (* Create a new map by applying a map function to the
76 (* Apply a folding function to the entries of the map
82 (* Apply a folding function to the entries of the map
94 (* map a partial function over the elements of a map in increasing
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | ord-map-sig.sml | 23 (* Update an item by applying a function to the item already stored.
54 * maps, using the supplied function to define the map on elements that
61 * two input maps, using the supplied function to define the range.
66 (* Apply a function to the entries of the map in map order. *)
70 (* Create a new map by applying a map function to the
76 (* Apply a folding function to the entries of the map
82 (* Apply a folding function to the entries of the map
94 (* map a partial function over the elements of a map in increasing
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | ord-map-sig.sml | 23 (* Update an item by applying a function to the item already stored.
54 * maps, using the supplied function to define the map on elements that
61 * two input maps, using the supplied function to define the range.
66 (* Apply a function to the entries of the map in map order. *)
70 (* Create a new map by applying a map function to the
76 (* Apply a folding function to the entries of the map
82 (* Apply a folding function to the entries of the map
94 (* map a partial function over the elements of a map in increasing
|
| /seL4-l4v-master/HOL4/src/portableML/poly/ |
| H A D | SHA1_ML.sig | 3 (* A reader assumes a stream or function view of IO. A reader function
|
| /seL4-l4v-master/HOL4/examples/bootstrap/ |
| H A D | source_syntaxScript.sml | 27 | Call name (exp list) (* call a function *)
35 prog = Program (dec list) exp (* function declarations followed by *)
|
| /seL4-l4v-master/HOL4/src/quotient/src/ |
| H A D | quotient.sig | 22 (* This file defines the function "define_quotient_type", which takes *)
35 (* The "define_quotient_type" function returns a theorem of the form *)
53 string -> (* name of abstraction function from old to new *)
54 string -> (* name of representation function from new to old *)
199 Thm.thm -> (* quotient theorem for domain of function *)
200 Thm.thm -> (* quotient theorem for range of function *)
201 Thm.thm (* returns quotient theorem for function:
224 fname : string, (* name of new function *)
225 func : Term.term, (* old function, to be lifted *)
226 fixity : Parse.fixity option} -> (* fixity of new function *)
[all...] |
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | acl2encodeLib.sig | 5 (* should be used in order of definition. Eg, if the function f calls the *)
6 (* function g, then g should be translated before f. Additionally, if *)
7 (* f takes as argument a type t, then a 'recognition' function must be *)
8 (* generated for t before it can be used. The function, *)
16 (* Missing rewrite: A function that is relied upon by the function *)
19 (* missing function, or flattening the recognizer for the required *)
20 (* type. If the function may not be translated automatically, *)
44 (* For a recursive function we must therefore prove two theorem forms. *)
53 (* found by using the function
[all...] |
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | FCNet.sig | 17 Provides a matching function that does the same.
|
| H A D | term_pp.sig | 10 (* this initialises a reference storing a function for pulling apart
|
| /seL4-l4v-master/HOL4/src/num/termination/ |
| H A D | selftest.sml | 4 val _ = tprint "Testing mutually recursive function definition"
41 val _ = tprint "Testing 0-arg recursive function with lambda"
47 val _ = tprint "Testing 1-arg recursive function with lambda"
53 val _ = tprint "Testing 2-arg recursive function with lambda"
|
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | defunctionalize.sml | 9 (* sion, no nested functions exist; and function call is made by dispatching on the closure*)
12 (* tion definition, a constructor taking the free variables of this function is created. *)
13 (* For each arrow type we create a dispatch function, which converts the definition of a *)
14 (* function of this arrow type into a closure constructor application. *)
15 (* A nested function is hoisted to the top level with its free variables to be passed as *)
16 (* extra arguments. After that, the calling to the original function is replaced by a *)
17 (* calling to the relevant dispatch function passing a closure containing the values of *)
18 (* this function's free variables. The dispatch function examines the closure tag and *)
19 (* passes control to the appropriate hoisted function
[all...] |