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,8893269a4640c798
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-07-22 05:59:33 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail
From: Lutz Donnerhacke <lutz@iks-jena.de>
Newsgroups: comp.lang.ada
Subject: Re: terminate applications
Date: Tue, 22 Jul 2003 12:59:33 +0000 (UTC)
Organization: IKS GmbH Jena
Message-ID: <slrnbhqd9i.oa.lutz@taranis.iks-jena.de>
References: <mailman.18.1058521718.24167.comp.lang.ada@ada.eu.org>
 <FlQRa.89768$H17.28202@sccrnsc02> <3F17DF3C.4080204@noplace.com>
 <KcURa.91888$H17.28020@sccrnsc02> <3F196773.2060809@noplace.com>
 <3F19F86C.9050808@attbi.com> <3F1A772F.9060708@noplace.com>
 <3F1AD6FB.8080806@attbi.com> <3F1BD666.6040506@noplace.com>
 <3F1C4DA6.3070405@attbi.com> <3F1D29E8.60107@noplace.com>
 <Pine.LNX.4.44.0307221421270.25598-100000@localhost.localdomain>
NNTP-Posting-Host: taranis.iks-jena.de
X-Trace: branwen.iks-jena.de 1058878773 4284 217.17.192.37 (22 Jul 2003
 12:59:33 GMT)
X-Complaints-To: usenet@iks-jena.de
NNTP-Posting-Date: Tue, 22 Jul 2003 12:59:33 +0000 (UTC)
User-Agent: slrn/0.9.7.4 (Linux)
Xref: archiver1.google.com comp.lang.ada:40636
Date: 2003-07-22T12:59:33+00:00
List-Id: <comp.lang.ada>

* Arnaud Charlet wrote:
>> I could probably go search through the Win32api and find a "Kill this 
>> process and I really, really mean it" system call, but a) it would be 
> 
> If that's what you're looking for (and it seems indeed pretty clear from
> your previous messages), then I'd suggest you ignore the other messages on
> this thread, and you do the same as with any other programming language:
> 
> procedure Halt;
> pragma Import (C, Halt, "exit");
> 
> ...
> Halt;
> 
> and be done with it.

That will start a clean shutdown of the libc. You don't won't that.

with Kernel.Processes;
[...]
   procedure Halt renames Kernel.Processes.sysexit;
   [...]
   Halt;

This is the right way! Read the spec:
   --  NAME
   --         exit - terminate the current process
   --  SYNOPSIS
   --         void _exit(int status);
   procedure sysexit (return_code : exit_code_t);
   --# global in out Kernel.State;
   --# derives Kernel.State from Kernel.State, return_code;
   pragma Inline_Always (sysexit);

and the implementation:

separate (Kernel.Processes)
procedure sysexit(return_code : exit_code_t) is
   UnusedRes : Linux_i86.syscall_result;
begin
   Linux_i86.syscall1(Linux_i86.sys_exit, long(return_code), UnusedRes); --! Assignment to UnusedRes is ineffective.
end sysexit; --! The variable UnusedRes is neither referenced nor exported.

and the exception freedom proof:

procedure_sysexit_1.
H1:  true.
H2:  return_code >= exit_code_t__first.
H3:  return_code <= exit_code_t__last.
        ->
C1:  return_code >= kernel__linux_i86__long__first.
C2:  return_code <= kernel__linux_i86__long__last.
C3:  kernel__linux_i86__sys_exit >= kernel__linux_i86__syscall_number__first.
C4:  kernel__linux_i86__sys_exit <= kernel__linux_i86__syscall_number__last.
C5:  return_code >= long__first.
C6:  return_code <= long__last.
 

*** Rule substitutions phase 1
*** Applied substitution rule sysexit_rules(4)
*** Applied substitution rule sysexit_rules(5)
*** Applied substitution rule sysexit_rules(3)
*** Applied substitution rule sysexit_rules(9)
*** Applied substitution rule sysexit_rules(10)
*** Applied substitution rule sysexit_rules(14)
*** Applied substitution rule sysexit_rules(15)
*** PROVED C3
*** PROVED C4
*** Rule substitutions phase 2
*** Applied substitution rule sysexit_rules(19)
*** Applied substitution rule sysexit_rules(20)
*** Standardise hypotheses
*** Standardise conclusions
*** PROVED C1
*** PROVED C2
*** PROVED C5
*** PROVED C6
*** Contradiction hunt
*** Proved all conclusions - VC eliminated
*** Expression reduction

          ==================================================

For path(s) from start to finish:

procedure_sysexit_2.
*** true .          /* trivially true VC removed by Examiner */

*** PROVED C1
*** Proved all conclusions - VC eliminated

Automatic simplification completed.

And don't do this with C!