search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Bad range when mistaking type #174

Open mtzguido opened 3 months ago

mtzguido commented 3 months ago

This raises two errors with a bad range. The mistake is that t is resolved to SizeT.t, while the user probably meant tt.

#lang-pulse

open Pulse
open FStar.SizeT

fn bad_range
  (#tt : Type0)
  (r : ref tt)
  (#v : erased tt)
  requires Pulse.Lib.Reference.pts_to r v
  ensures  Pulse.Lib.Reference.pts_to r v
{
  let v = Pulse.Lib.Reference.op_Bang #t r;
  admit();
}
* Error 19 at pulse/X.fst(8,0-17,1):                            # All of the definition
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - Also see: pulse/X.fst(10,11-15,37)                          # From the `tt` in the binder `r` up to `op_Bang`
  - Other related locations: pulse/X.fst(15,39-15,40)           # Points to the `#t`
  - Raised within Tactics.refl_tc_term

* Error 228 at pulse/X.fst(8,0-17,1):                           # All of the definition
  - Ill-typed term:!r

image