Re: terminate applications

[Lutz Donnerhacke <lutz@iks-jena.de>]

* 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!