/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | float.c | 11 static int floating(int a, float b, double c, long double d) function 50 floating (si1, f, d, ld); 52 ffi_call(&cif, FFI_FN(floating), &rint, values); 54 printf ("%d vs %d\n", (int)rint, floating (si1, f, d, ld)); 56 CHECK((int)rint == floating(si1, f, d, ld));
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src-base/ |
H A D | pide_docking_framework.scala | 38 case floating: FloatingWindowContainer => 39 Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src-base/ |
H A D | pide_docking_framework.scala | 38 case floating: FloatingWindowContainer => 39 Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | mos.ml | 6 % (or floating) and undefined/unknown respectively. %
|
/seL4-l4v-10.1.1/HOL4/src/float/ |
H A D | ieeeScript.sml | 3 (* Formalization of IEEE-754 Standard for binary floating-point arithmetic. *) 29 (* Derived parameters for floating point formats. *) 156 (* Negation operation on floating point values. *) 226 (* Rounding to floating point formats. *) 254 (* Rounding to integer values in floating point format. *)
|
H A D | floatScript.sml | 2 Useful properties of floating point numbers.
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 304 (* RTS call with one double-precision floating point argument and a floating point result. 366 (* Put the floating point result into a box. *) 403 (* RTS call with one general (i.e. ML word) argument and a floating point result. 456 (* Put the floating point result into a box. *)
|
H A D | X86CODESIG.sml | 60 val allRegisters: regSet (* All registers: data, address, floating pt. *)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | BUILTINS.sml | 62 | FloatFixedInt (* Convert an integer value into a floating point value. *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | ppc_closure.S | 45 # in registers (both floating point and integer)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sparc/ |
H A D | v9.S | 158 ! Store possible floating point argument registers too.
|
/seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 109 (* floating pointt configurations *)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 356 , 13-12 : MFS -- floating-point context status 457 , 13-12 : SFS -- floating-point context status 493 -- floating point control and status 652 c_fpr :: id -> RegFile -- floating-point registers 911 { -- user floating-point context 1018 { -- user floating-point context 1117 { -- user floating-point context 1252 fp_data :: fpval option -- floating point value
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/x86/ |
H A D | win32.S | 114 ;; obliged to handle floating-point values. 601 # obliged to handle floating-point values.
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_FUNCTIONS.sml | 118 (* If we float a 64-bit int to a 64-bit floating point value we may
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | binary_ieeeScript.sml | 2 Theory of IEEE-754 (base 2) floating-point (basic) arithmetic 24 Binary floating point representation 157 Rounding reals to floating-point values
|
H A D | lift_ieeeScript.sml | 2 Some basic properties of IEEE-754 (base 2) floating-point arithmetic
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_stepScript.sml | 125 (* For floating-point single precision access *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 349 Exponentiation can express floating-point values such as
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 349 Exponentiation can express floating-point values such as
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 707 \item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) 709 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 707 \item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) 709 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 203 impressive integer and floating-point examples (see the DAC98
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 203 impressive integer and floating-point examples (see the DAC98
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 133 (* Return the argument/result type which is currently just floating point or everything else. *)
|