Mentions légales du service

Skip to content
  • Johannes Kanig's avatar
    P909-002 allow for large exit codes · 883af7f6
    Johannes Kanig authored
    Sometimes the windows syscall GetExitCodeProcess returns a large result,
    larger than the ocaml [int] type. This is expected and not an error. For
    example the constant STATUS_QUOTA_EXCEEDED, which is 0xC0000044, may be
    a valid exit code. Such large values trip up the [int_of_string] parsing
    in the client.
    
    This patch implements the following solution to this problem:
    * the server doesn't care and sends the large value;
    * (the server now recognizes this value, though, to set the timeout flag
      more often)
    * the client uses an Int64 value to parse that big constant;
    * when converting to the internal Unix.process_status type, we simply
      convert to [int], because such large values don't have any special
      meaning for Why3 anyway.
    
    * call_provers.ml
    (parse_prover_run): now directly take the exit status as argument, and
    convert it to int;
    (handle_answer): don't wrap argument to parse_prover_run into unix type
    * prove_client.ml
    (read_answer): read Int64 type now
    * server-win.c
    (handle_child_event): set timeout boolean also when exitcode is equal to
       constant STATUS_QUOTA_EXCEEDED
    
    Change-Id: I1163a6f1adf1bdbfe1f53269ce0ae57dc8bd0287
    883af7f6