From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,60e2922351e0e780 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-11-24 02:20:03 PST Path: archiver1.google.com!news2.google.com!fu-berlin.de!newsfeed.vmunix.org!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail From: Lutz Donnerhacke Newsgroups: comp.lang.ada Subject: Re: Generic thinbinding toolkit for C Date: Mon, 24 Nov 2003 10:20:00 +0000 (UTC) Organization: IKS GmbH Jena Message-ID: References: <3FB0B57D.6070906@noplace.com> <3FB22125.1040807@noplace.com> <3FB3751D.5090809@noplace.com> <3FB8B9BC.5040505@noplace.com> <3FBA1118.4060105@noplace.com> <0fxub.48425$bQ3.12107@nwrdny03.gnilink.net> <3FBC2EEC.212A1B5@cogeco.ca> <3FBEF03D.6E3474BE@nospam.cogeco.ca> NNTP-Posting-Host: taranis.iks-jena.de X-Trace: branwen.iks-jena.de 1069669200 1692 217.17.192.37 (24 Nov 2003 10:20:00 GMT) X-Complaints-To: usenet@iks-jena.de NNTP-Posting-Date: Mon, 24 Nov 2003 10:20:00 +0000 (UTC) User-Agent: slrn/0.9.7.4 (Linux) Xref: archiver1.google.com comp.lang.ada:2893 Date: 2003-11-24T10:20:00+00:00 List-Id: * Warren Gay wrote: > Note also that because you're starting with C code, I don't expect > the resulting thin binding to be strongly typed. It might be stronger > with the help of hints/config entries, but I would not have the > unrealistic expectation that the spec is going to be strongly typed. Currently I get a strongly typed thin binding. The generated object code contains a single "INT 80" line in most cases. Your proposal with wrapper bindings works an can be automated. Intrestingly enough you do not need any tool for this job, because you have to specify the necessary API yourself (it can't be derivated from the header files as proven upthreads). When you did this, you are finished anyway, because you have the wrapper code and directly importable linker objects for Ada. Done. > That is the job for the thick binding, which is now easier for you to > write! Thick binding is completely different. For thick binding you redesign the API the Ada way. Then you transform this API to the called library API. I prefer stronly typed thin bindings. This is an slightly expanded API very close to the original one. The only enhancements consist of Ada style parameter passing, Ada style constants and semantically different types based on the same implementation type (i.e. type Filename is new C_String;) > I can call getuid() from Ada, almost as easily as I can from C. The > _problem_ is that I don't have a spec for that function (with the > matching sized type), for every platform. Yep. > With a generated thin binding that includes the necessary spec, > calling getuid() from Ada becomes effortless and is in all other > respects, including efficiency, on par with C. Because you don't have the size of the types, you have to introduce a level of indirection into the wrapper code. You can't access those values, unless you use wrapper code as well. Therefor every wrapper will copy data twice or more to call the library. This will be inefficient at least. > So if I can determine the size and types of the return value for getuid(), > then there is no reason thinbind cannot generate a spec, a type (if > necessary), and a pragma import statement. In this case, no > C wrapper code is required and everyone is still happy. You will generate an Ada-Spec from external programms? You will get horrible problems with compile time errors at the Ada side when switching to a different platform? Good luck. >> This hints file has to contain the API, because it can't regained from the >> C header code (too much type information is missing). > > This of course, depends on how far down the road to compiling > you want to go. The C compiler knows about types. There is no > theoretical reason that thinbind could not also (only the amount > of complexity and work, but no worse than GCC). The C compiler does know nothing about types. The real types are defined in the semantics (man page). The C compiler does know only about base types. > You constantly look for defeat. Look for solutions: that's what > programmers normally do. Otherwise, we might as well shut everything down > and say "it's too hard", and watch golf instead. Ada style solution: 1.0k kernel.ads 27k kernel-calls.adb 601k kernel-calls.ads 26k kernel-linux_i86.adb 29k kernel-linux_i86.ads Example: .file "test_kernel.adb" .version "01.01" gcc2_compiled.: .section .rodata .LC0: .string "kernel-linux_i86.adb" .LC1: .string "kernel-calls.adb" .LC2: .ascii "Hello world.\n" .data .type outs.68,@object .size outs.68,13 outs.68: .ascii "Hello world.\n" .text .align 4 .globl _start .type _start,@function _start: pushl %esi pushl %ebx movl $4,%eax movl $1,%ebx movl $outs.68,%ecx movl $13,%edx #APP int $0x80 #NO_APP movl %eax,%esi movl %ebx,%eax movl %esi,%ebx #APP int $0x80 #NO_APP popl %ebx popl %esi ret .Lfe1: .size _start,.Lfe1-_start .ident "GCC: (GNU) 2.8.1" Spark style solution: 1.0k kernel.ads 3.0k kernel-io.adb 12k kernel-io.ads 1.0k kernel-io-chdir.adb 1.0k kernel-io-close.adb 1.0k kernel-io-creat.adb 1.0k kernel-io-fchdir.adb 1.0k kernel-io-fullpath_to_long.adb 2.0k kernel-io-getdents.adb 1.0k kernel-io-getdents_empty.adb 2.0k kernel-io-getdents_read.adb 1.0k kernel-io-integer_to_permissions.adb 1.0k kernel-io-link.adb 1.0k kernel-io-llseek.adb 1.0k kernel-io-mkdir.adb 2.0k kernel-io-mode_to_string.adb 1.0k kernel-io-open.adb 1.0k kernel-io-open_flags_to_long.adb 1.0k kernel-io-permissions_to_integer.adb 1.0k kernel-io-permission_to_string.adb 1.0k kernel-io-read.adb 1.0k kernel-io-rename.adb 1.0k kernel-io-string_to_fullpath.adb 1.0k kernel-io-string_to_long.adb 1.0k kernel-io-unlink.adb 1.0k kernel-io-write.adb 6.0k kernel-linux_i86.adb 26k kernel-linux_i86.ads 3.0k kernel-processes.adb 7.0k kernel-processes.ads 1.0k kernel-processes-cstring_array_from_collection.adb 1.0k kernel-processes-cstring_nul_count.adb 1.0k kernel-processes-fork.adb 1.0k kernel-processes-kill_all.adb 1.0k kernel-processes-kill_group.adb 1.0k kernel-processes-kill_my_group.adb 1.0k kernel-processes-kill_process.adb 1.0k kernel-processes-signal_to_long.adb 1.0k kernel-processes-sysexit.adb 1.0k kernel-processes-wait.adb 1.0k kernel-processes-wait_group.adb 1.0k kernel-processes-wait_my_group.adb 3.0k kernel-processes-waitpid.adb 1.0k kernel-processes-wait_process.adb ------------------------------------------------------------------------------- Semantic Analysis Summary ------------------------------------------------------------------------------- Summary of: Verification Condition files (.vcg) Simplified Verification Condition files (.siv) in the directory: /var/home/lutz/work/ada/src/kernel VCs for kernel_/processes/cstring_nul_count ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 7 | DOIT 2 | start | assert @ 7 | DOIT 3 | assert @ 7 | assert @ 7 | yes 4 | assert @ 7 | assert @ 7 | yes 5 | assert @ 7 | rtc check @ 10 | yes 6 | assert @ 7 | rtc check @ 11 | DOIT 7 | start | finish | yes 8 | assert @ 7 | finish | DOIT 9 | assert @ 7 | finish | yes ------------------------------------------------------------------------------- VC Hashs for kernel_/processes/cstring_nul_count 1 : efe586a0bd3de1bb8b8f2cc880f46a98 2 : 75e2c969ead1d0dea799bf625d14e3a7 6 : 4d2360999a219c96aa8045a50b190c05 8 : 673f9713dfc6afd15b10a0e3a4e30cdf VCs for kernel_/io/write ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 9 | yes 2 | start | rtc check @ 10 | yes 3 | start | check @ 11 | yes 4 | start | rtc check @ 12 | yes 5 | start | rtc check @ 12 | yes 6 | start | rtc check @ 16 | yes 7 | start | rtc check @ 17 | DOIT 8 | start | rtc check @ 19 | yes 9 | start | rtc check @ 20 | yes 10 | start | rtc check @ 23 | yes 11 | start | finish | yes 12 | start | finish | yes 13 | start | finish | yes ------------------------------------------------------------------------------- VC Hashs for kernel_/io/write 7 : dc437863df9e7bbc38a3b6a01eea04aa VCs for kernel_/linux_i86/syscall1 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 62 | yes 2 | start | rtc check @ 63 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/mode_to_string ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 21 | yes 2 | start | rtc check @ 28 | yes 3 | start | rtc check @ 29 | yes 4 | start | assert @ 32 | yes 5 | start | assert @ 32 | yes 6 | start | assert @ 32 | yes 7 | assert @ 32 | rtc check @ 34 | yes 8 | assert @ 32 | rtc check @ 35 | yes 9 | assert @ 32 | assert @ 38 | yes 10 | assert @ 32 | assert @ 38 | yes 11 | assert @ 32 | assert @ 38 | yes 12 | assert @ 38 | rtc check @ 40 | yes 13 | assert @ 38 | rtc check @ 41 | yes 14 | assert @ 38 | assert @ 44 | yes 15 | assert @ 38 | assert @ 44 | yes 16 | assert @ 38 | assert @ 44 | yes 17 | assert @ 44 | rtc check @ 46 | yes 18 | assert @ 44 | rtc check @ 47 | yes 19 | assert @ 44 | rtc check @ 48 | yes 20 | assert @ 44 | rtc check @ 49 | yes 21 | assert @ 44 | rtc check @ 50 | yes 22 | assert @ 44 | rtc check @ 51 | yes 23 | assert @ 44 | rtc check @ 52 | yes 24 | assert @ 44 | finish | yes 25 | assert @ 44 | finish | yes 26 | assert @ 44 | finish | yes 27 | assert @ 44 | finish | yes 28 | assert @ 44 | finish | yes 29 | assert @ 44 | finish | yes 30 | assert @ 44 | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/open ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | rtc check @ 10 | yes 3 | start | rtc check @ 11 | yes 4 | start | rtc check @ 13 | yes 5 | start | rtc check @ 14 | yes 6 | start | rtc check @ 17 | yes 7 | start | finish | yes 8 | start | finish | yes 9 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/chdir ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/wait_group ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 7 | yes 2 | start | rtc check @ 8 | yes 3 | start | rtc check @ 9 | yes 4 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/syscall4 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 134 | yes 2 | start | rtc check @ 135 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/close ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 5 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/link ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/getdents ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 21 | yes 2 | start | rtc check @ 21 | yes 3 | start | rtc check @ 24 | yes 4 | start | rtc check @ 25 | yes 5 | start | rtc check @ 27 | yes 6 | start | rtc check @ 29 | yes 7 | start | finish | yes 8 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/creat ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | rtc check @ 9 | yes 3 | start | rtc check @ 10 | yes 4 | start | rtc check @ 12 | yes 5 | start | rtc check @ 13 | yes 6 | start | rtc check @ 16 | yes 7 | start | finish | yes 8 | start | finish | yes 9 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/kill_my_group ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | rtc check @ 6 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/waitpid ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 77 | yes 2 | start | rtc check @ 82 | yes 3 | start | rtc check @ 83 | yes 4 | start | rtc check @ 85 | yes 5 | start | finish | yes 6 | start | finish | yes 7 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/syscall0 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 38 | yes 2 | start | rtc check @ 39 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/wait ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/permission_to_string ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 7 | yes 2 | start | rtc check @ 8 | yes 3 | start | rtc check @ 8 | yes 4 | start | rtc check @ 9 | yes 5 | start | rtc check @ 9 | yes 6 | start | rtc check @ 9 | yes 7 | start | rtc check @ 9 | yes 8 | start | finish | yes 9 | start | finish | yes 10 | start | finish | yes 11 | start | finish | yes 12 | start | finish | yes 13 | start | finish | yes 14 | start | finish | yes 15 | start | finish | yes ------------------------------------------------------------------------------- VCs for test_kernel ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 16 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/unlink ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/kill_all ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 5 | yes 2 | start | rtc check @ 5 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/open_flags_to_long ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 14 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/wait_my_group ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/read ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | rtc check @ 6 | yes 3 | start | rtc check @ 11 | yes 4 | start | rtc check @ 12 | yes 5 | start | finish | yes 6 | start | finish | yes 7 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/fchdir ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 5 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/getdents_read ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 34 | yes 2 | start | rtc check @ 35 | yes 3 | start | rtc check @ 39 | yes 4 | start | rtc check @ 40 | yes 5 | start | rtc check @ 43 | yes 6 | start | rtc check @ 44 | yes 7 | start | rtc check @ 45 | yes 8 | start | rtc check @ 46 | yes 9 | start | rtc check @ 46 | yes 10 | start | assert @ 46 | yes 11 | assert @ 46 | assert @ 46 | yes 12 | assert @ 46 | rtc check @ 49 | yes 13 | assert @ 46 | rtc check @ 50 | yes 14 | start | rtc check @ 57 | yes 15 | start | rtc check @ 57 | yes 16 | assert @ 46 | rtc check @ 57 | yes 17 | assert @ 46 | rtc check @ 57 | yes 18 | start | finish | yes 19 | start | finish | yes 20 | start | finish | yes 21 | start | finish | yes 22 | assert @ 46 | finish | yes 23 | assert @ 46 | finish | yes 24 | assert @ 46 | finish | yes 25 | assert @ 46 | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/syscall5 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 158 | yes 2 | start | rtc check @ 159 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/string_to_fullpath ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | assert @ 6 | yes 3 | assert @ 6 | assert @ 6 | yes 4 | assert @ 6 | rtc check @ 9 | yes 5 | start | rtc check @ 11 | yes 6 | assert @ 6 | rtc check @ 11 | yes 7 | start | finish | yes 8 | assert @ 6 | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/sysexit ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/kill_process ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | rtc check @ 6 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/fork ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 5 | yes 2 | start | rtc check @ 6 | yes 3 | start | rtc check @ 8 | yes 4 | start | rtc check @ 9 | yes 5 | start | rtc check @ 13 | yes 6 | start | finish | yes 7 | start | finish | yes 8 | start | finish | yes 9 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/getdents_empty ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/wait_process ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/errorcode ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 9 | yes 2 | start | rtc check @ 10 | yes 3 | start | rtc check @ 12 | yes 4 | start | finish | yes 5 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/processes/kill_group ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 7 | yes 2 | start | rtc check @ 8 | yes 3 | start | rtc check @ 9 | yes 4 | start | rtc check @ 9 | yes 5 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/syscall3 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 110 | yes 2 | start | rtc check @ 111 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/mkdir ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/linux_i86/syscall2 ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 86 | yes 2 | start | rtc check @ 87 | yes 3 | start | finish | yes ------------------------------------------------------------------------------- VCs for kernel_/io/rename ------------------------------------------------------------------------------- | | | -- Proved In -- No | From | To | vcg siv plg prv TODO ------------------------------------------------------------------------------- 1 | start | rtc check @ 6 | yes 2 | start | finish | yes ------------------------------------------------------------------------------- =============================================================================== --------------- Proved By -------------- Total Examiner Simplifier Checker Review Undischarged Assert 16 0 15 0 0 1 Check 1 0 1 0 0 0 Postcondition 76 28 47 0 0 1 Runtime check 124 0 121 0 0 3 ------------------------------------------------------------------------------- Totals 217 28 184 0 0 5 % Totals 12% 84% 0% 0% 2% ===================== End of Semantic Analysis Summary ======================== > I don't know about you, but watching golf puts me to sleep ;-) I prefer to program myself, instead of wait for a generic solution. > Be positive. It helps. I prefer matching Ada solutions over generated Ada syntax from C code.