;;;; (slice-from-ptr p n) with a length the checker cannot see.
;;;;
;;;; test/programs/slice-from-ptr.flan covers the form itself, but every length
;;;; in it is a literal, and a negative literal is refused by check.ml before
;;;; any code is emitted. So the run-time half of the check -- the one both
;;;; backends plant beside the form -- is walked by nothing in the corpus.
;;;;
;;;; The half that matters here is that the test is *signed*. check_slice's own
;;;; compares are unsigned, and a negative i32 sign-extended to 64 bits is a
;;;; huge unsigned value that an unsigned "hi <= len" waves straight through.
;;;; Getting that wrong yields a slice whose length is about 2^64, which reads
;;;; as a pass and segfaults somewhere else entirely.
;;;;
;;;; Both cases go through a restart-case, so what is compared is the message
;;;; on stderr as well as the fact that something was signalled.

(defvar a [4 i32])

(defn promised [n i32] i32
  ;; n is a parameter, so the checker has no literal to look at.
  (restart-case
    (let [s (slice-from-ptr (addr (at a 0)) n)]
      (len s))
    (give-up [] -1)))

(defn show [name string n i64] ()
  (print name)
  (print " ")
  (println n))

(defn main [] ()
  (dotimes [i 4]
    (set (at a i) (* (+ i 1) 10)))

  (handler-bind
    [(BoundsError [c]
       (show "low" (.low c))
       (show "high" (.high c))
       (show "length" (.length c))
       (invoke-restart 'give-up))]

    (println (promised 4))          ; 4  -- the truth
    (println (promised 0))          ; 0  -- empty is not an error
    (println (promised 2))          ; 2  -- shorter than the truth is legal
    (println (promised -1))         ; -1 -- signalled, and the restart answered
    (println (promised -1000000))))