Improve test.

gebner · gebner · commit 0b990e047ac5 · 2026-05-07T03:21:22.000Z
diff --git a/test/refine_uninit.c b/test/refine_uninit.c
@@ -2,11 +2,11 @@
 #include "pal.h"
 #include <stdint.h>
 
-_refine_uninit((_slprop) _inline_pulse(pure (is_null $(this))))
+_refine_uninit((bool) _inline_pulse(is_null $(this)))
 typedef int *nullable_ptr;
 
-void take_nullable(_plain nullable_ptr p)
-    _requires((_slprop) _inline_pulse(pure (is_null $(p))))
-    _ensures((_slprop) _inline_pulse(pure (is_null $(p))))
+void take_nullable(_out nullable_ptr p)
 {
+    _ghost_stmt(Pulse.Lib.Reference.pts_to_uninit_not_null $(p));
+    _ghost_stmt(unreachable());
 }

Original file line number	Diff line number	Diff line change
`@@ -2,11 +2,11 @@`
`2`	`2`	`#include "pal.h"`
`3`	`3`	`#include <stdint.h>`
`4`	`4`
`5`		`-_refine_uninit((_slprop) _inline_pulse(pure (is_null $(this))))`
	`5`	`+_refine_uninit((bool) _inline_pulse(is_null $(this)))`
`6`	`6`	`typedef int *nullable_ptr;`
`7`	`7`
`8`		`-void take_nullable(_plain nullable_ptr p)`
`9`		`- _requires((_slprop) _inline_pulse(pure (is_null $(p))))`
`10`		`- _ensures((_slprop) _inline_pulse(pure (is_null $(p))))`
	`8`	`+void take_nullable(_out nullable_ptr p)`
`11`	`9`	`{`
	`10`	`+ _ghost_stmt(Pulse.Lib.Reference.pts_to_uninit_not_null $(p));`
	`11`	`+ _ghost_stmt(unreachable());`
`12`	`12`	`}`