SliceRef also needs the slice element type

Author: RalfJung

goose.go

@@ -901,8 +901,9 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 	if e.Op == token.AND {
 		if x, ok := e.X.(*ast.IndexExpr); ok {
 			// e is &a[b] where x is a.b
-			if _, ok := ctx.typeOf(x.X).(*types.Slice); ok {
+			if xTy, ok := ctx.typeOf(x.X).(*types.Slice); ok {
 				return coq.NewCallExpr("SliceRef",
+					ctx.coqTypeOfType(e, xTy.Elem()),
 					ctx.expr(x.X), ctx.expr(x.Index))
 			}
 		}

internal/examples/semantics/semantics.gold.v

@@ -1265,7 +1265,7 @@ Definition testSliceOps: val :=
     let: "v1" := SliceGet uint64T "x" #2 in
     let: "v2" := SliceSubslice uint64T "x" #2 #3 in
     let: "v3" := SliceTake "x" #3 in
-    let: "v4" := SliceRef "x" #2 in
+    let: "v4" := SliceRef uint64T "x" #2 in
     let: "ok" := ref_to boolT #true in
     "ok" <-[boolT] (![boolT] "ok") && ("v1" = #10);;
     "ok" <-[boolT] (![boolT] "ok") && (SliceGet uint64T "v2" #0 = #10);;

internal/examples/unittest/unittest.gold.v

@@ -752,7 +752,7 @@ Definition sliceOps: val :=
     let: "v1" := SliceGet uint64T "x" #2 in
     let: "v2" := SliceSubslice uint64T "x" #2 #3 in
     let: "v3" := SliceTake "x" #3 in
-    let: "v4" := SliceRef "x" #2 in
+    let: "v4" := SliceRef uint64T "x" #2 in
     "v1" + SliceGet uint64T "v2" #0 + SliceGet uint64T "v3" #1 + ![uint64T] "v4".
 
 Definition makeSingletonSlice: val :=
@@ -769,7 +769,7 @@ Definition sliceOfThings := struct.decl [
 
 Definition sliceOfThings__getThingRef: val :=
   rec: "sliceOfThings__getThingRef" "ts" "i" :=
-    SliceRef (struct.get sliceOfThings "things" "ts") "i".
+    SliceRef (struct.t thing) (struct.get sliceOfThings "things" "ts") "i".
 
 Definition makeAlias: val :=
   rec: "makeAlias" <> :=