diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 82a079e98bd4fab78b03020d910170aaa3b64b1e..226cab728c71b687a44893152ae307cd1af3e012 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -51,11 +51,7 @@ extern int pselect(int nfds, fd_set * readfds,
   requires errorfds: errorfds == \null || \valid(errorfds);
   requires timeout: timeout == \null || \valid(timeout);
   assigns __fc_fds_state \from __fc_fds_state;
-  assigns readfds  == \null ? \empty : *readfds,
-          writefds == \null ? \empty : *writefds,
-          errorfds == \null ? \empty : *errorfds,
-          timeout == \null ? \empty : *timeout,
-          \result
+  assigns *readfds, *writefds, *errorfds, *timeout, \result
     \from indirect:nfds,
           indirect:readfds, indirect:*readfds,
           indirect:writefds, indirect:*writefds,
diff --git a/share/libc/signal.h b/share/libc/signal.h
index f42d35711ab12190c0f7e2900f36ce4a2b922333..27ae78965980e8df8e4473bf131b5c445da1faa8 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -205,8 +205,8 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
   requires valid_oldact_or_null: oldact == \null || \valid(oldact);
   requires valid_read_act_or_null: act == \null || \valid_read(act);
   requires separation:separated_acts: \separated(act, oldact);
-  assigns oldact == \null ? \empty : *oldact \from __fc_p_sigaction;
-  assigns act == \null ? \empty : __fc_p_sigaction[signum] \from *act;
+  assigns *oldact \from __fc_p_sigaction;
+  assigns __fc_p_sigaction[signum] \from *act;
   assigns \result \from indirect:signum, indirect:act, indirect:*act,
                         indirect:oldact, indirect:*oldact;
   ensures act_changed: act == \null || \subset(__fc_p_sigaction[signum], *act);
@@ -225,8 +225,7 @@ extern int sigaction(int signum, const struct sigaction *restrict act,
   requires separation: (set == oldset == \null) ||
                        \separated(set, oldset);
   assigns \result \from indirect:how, indirect:set, indirect:oldset;
-  assigns oldset == \null ? \empty : *oldset
-          \from indirect:how, indirect:oldset;
+  assigns *oldset \from indirect:how, indirect:oldset;
   ensures result_ok_or_error: \result == 0 || \result == -1;
   ensures initialization:oldset_initialized:
     oldset != \null && \result == 0 ==> \initialized(oldset);
diff --git a/share/libc/stropts.h b/share/libc/stropts.h
index 48351585e7e3537806592d6ac9d2d6cf81d9f2af..3b0ee82968b303fbf98723c0d45d05198c11e4ea 100644
--- a/share/libc/stropts.h
+++ b/share/libc/stropts.h
@@ -172,7 +172,7 @@ extern int    __va_ioctl_int(int fd, int request, int arg);
 
 /*@ assigns \result \from indirect:fd, indirect:request,
       indirect:((char*)argp)[0..];
-    assigns argp != \null ? ((char*)argp)[0..] : \empty \from
+    assigns ((char*)argp)[0..] \from
       indirect:fd, indirect:request, ((char*)argp)[0..]; */
 extern int    __va_ioctl_ptr(int fd, int request, void* argp);
 
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 73fed482445f4c6a663ae88e8535b45fc5c704a8..b860763f4d3909a5c198a66af5701417801f78c9 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -151,16 +151,16 @@ extern int getitimer(int which, struct itimerval *curr_value);
 /*@
   requires valid_new_value: \valid_read(new_value);
   requires old_value_null_or_valid: old_value == \null || \valid(old_value);
-  assigns old_value != \null ? *old_value : \empty \from
-    indirect:which, indirect:old_value, indirect:new_value,
-    __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+  assigns *old_value \from indirect:which, indirect:old_value,
+                           indirect:new_value, __fc_itimer_real,
+                           __fc_itimer_virtual, __fc_itimer_prof;
   assigns \result \from indirect:which, indirect:new_value, indirect:*new_value;
   ensures result_ok_or_error: \result == 0 || \result == -1;
   behavior real:
     assumes itimer_real_and_valid:
       which == ITIMER_REAL && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty \from __fc_itimer_real;
+    assigns *old_value \from __fc_itimer_real;
     assigns __fc_itimer_real \from *new_value;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
@@ -168,14 +168,14 @@ extern int getitimer(int which, struct itimerval *curr_value);
     assumes itimer_virtual_and_valid:
       which == ITIMER_VIRTUAL && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty  \from __fc_itimer_virtual;
+    assigns *old_value \from __fc_itimer_virtual;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
   behavior prof:
     assumes itimer_prof_and_valid:
       which == ITIMER_PROF && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty  \from __fc_itimer_prof;
+    assigns *old_value \from __fc_itimer_prof;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
   behavior invalid:
diff --git a/share/libc/time.h b/share/libc/time.h
index 60e5031571f9ef5e2d527e9b5e8a81907ae66a36..52c66700cc80c3df73b708b8f6a302a30b2d6877 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -216,9 +216,8 @@ extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
     assumes no_einval: valid_clock_id(clock_id);
     assigns \result \from indirect:__fc_time, indirect:clock_id, indirect:rqtp,
                           indirect:*rqtp;
-    assigns rmtp == \null ? \empty : *rmtp \from __fc_time, indirect:clock_id,
-                                                 indirect:rqtp, indirect:*rqtp,
-                                                 indirect:rmtp;
+    assigns *rmtp \from __fc_time, indirect:clock_id, indirect:rqtp,
+                        indirect:*rqtp, indirect:rmtp;
     ensures result_interrupted: \result == EINTR;
     ensures initialization:interrupted_remaining:
       rmtp != \null ==> \initialized(&rmtp->tv_sec) && \initialized(&rmtp->tv_nsec);
@@ -263,9 +262,8 @@ extern struct tm *localtime_r(const time_t *restrict timep,
   requires valid_nanosecs: 0 <= rqtp->tv_nsec < 1000000000;
   requires valid_remaining_or_null: rmtp == \null || \valid(rmtp);
   assigns \result \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp;
-  assigns rmtp == \null ? \empty : *rmtp \from indirect:__fc_time,
-                                               indirect:rqtp, indirect:*rqtp,
-                                               indirect:rmtp;
+  assigns *rmtp \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp,
+                      indirect:rmtp;
   ensures result_elapsed_or_interrupted: \result == 0 || \result == -1;
   ensures initialization:interrupted_remaining:
     rmtp != \null && \result == -1 ==>
diff --git a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
index 834a0dde5f6db9f527a604df92cba0f2fa2a7226..195847c4a798c48e04d7613f0a9ff77e106c4001 100644
--- a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
@@ -13,6 +13,9 @@
 [eva] Initial state computed
 [eva] using specification for function __va_ioctl_void
 [eva] using specification for function __va_ioctl_ptr
+[eva:invalid-assigns] tests/known/ioctl.c:17: 
+  Completely invalid destination for assigns clause *((char *)argp + (0 ..)).
+  Ignoring.
 [eva] using specification for function __va_ioctl_int
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 107f92c67f3f62604ce53ca25bf5a5672e0c65be..417ea214e24ff7f7103182badf324309869ad81f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3145,10 +3145,9 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
         \old(oldact) ≡ \null ∨
         *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
-    assigns oldact ≡ \null? \empty: *oldact,
-            act ≡ \null? \empty: *(__fc_p_sigaction + signum), \result;
-    assigns oldact ≡ \null? \empty: *oldact \from __fc_p_sigaction;
-    assigns act ≡ \null? \empty: *(__fc_p_sigaction + signum) \from *act;
+    assigns *oldact, *(__fc_p_sigaction + signum), \result;
+    assigns *oldact \from __fc_p_sigaction;
+    assigns *(__fc_p_sigaction + signum) \from *act;
     assigns \result
       \from (indirect: signum), (indirect: act), (indirect: *act),
             (indirect: oldact), (indirect: *oldact);
@@ -3166,11 +3165,10 @@ extern int sigaction(int signum, struct sigaction const * __restrict act,
       initialization: oldset_initialized:
         \old(oldset) ≢ \null ∧ \result ≡ 0 ⇒
         \initialized(\old(oldset));
-    assigns \result, oldset ≡ \null? \empty: *oldset;
+    assigns \result, *oldset;
     assigns \result
       \from (indirect: how), (indirect: set), (indirect: oldset);
-    assigns oldset ≡ \null? \empty: *oldset
-      \from (indirect: how), (indirect: oldset);
+    assigns *oldset \from (indirect: how), (indirect: oldset);
  */
 extern int sigprocmask(int how, sigset_t const * __restrict set,
                        sigset_t * __restrict oldset);
@@ -5840,11 +5838,11 @@ axiomatic nanosleep_predicates {
       ensures
         remaining_valid:
           \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
-      assigns \result, rmtp ≡ \null? \empty: *rmtp;
+      assigns \result, *rmtp;
       assigns \result
         \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
               (indirect: *rqtp);
-      assigns rmtp ≡ \null? \empty: *rmtp
+      assigns *rmtp
         \from __fc_time, (indirect: clock_id), (indirect: rqtp),
               (indirect: *rqtp), (indirect: rmtp);
     
@@ -5901,10 +5899,10 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
       interrupted_remaining_valid:
         \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
         0 ≤ \old(rmtp)->tv_nsec < 1000000000;
-    assigns \result, rmtp ≡ \null? \empty: *rmtp;
+    assigns \result, *rmtp;
     assigns \result
       \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
-    assigns rmtp ≡ \null? \empty: *rmtp
+    assigns *rmtp
       \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
             (indirect: rmtp);
  */
@@ -6753,8 +6751,8 @@ extern int getitimer(int which, struct itimerval *curr_value);
     requires
       old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
-    assigns old_value ≢ \null? *old_value: \empty, \result;
-    assigns old_value ≢ \null? *old_value: \empty
+    assigns *old_value, \result;
+    assigns *old_value
       \from (indirect: which), (indirect: old_value), (indirect: new_value),
             __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
     assigns \result
@@ -6767,10 +6765,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty,
-              __fc_itimer_real;
+      assigns \result, *old_value, __fc_itimer_real;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_real;
+      assigns *old_value \from __fc_itimer_real;
       assigns __fc_itimer_real \from *new_value;
     
     behavior virtual:
@@ -6780,10 +6777,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty;
+      assigns \result, *old_value;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty
-        \from __fc_itimer_virtual;
+      assigns *old_value \from __fc_itimer_virtual;
     
     behavior prof:
       assumes
@@ -6792,9 +6788,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty;
+      assigns \result, *old_value;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_prof;
+      assigns *old_value \from __fc_itimer_prof;
     
     behavior invalid:
       assumes
@@ -6818,27 +6814,25 @@ extern int setitimer(int which,
     requires writefds: writefds ≡ \null ∨ \valid(writefds);
     requires errorfds: errorfds ≡ \null ∨ \valid(errorfds);
     requires timeout: timeout ≡ \null ∨ \valid(timeout);
-    assigns __fc_fds_state, readfds ≡ \null? \empty: *readfds,
-            writefds ≡ \null? \empty: *writefds,
-            errorfds ≡ \null? \empty: *errorfds,
-            timeout ≡ \null? \empty: *timeout, \result;
+    assigns __fc_fds_state, *readfds, *writefds, *errorfds, *timeout,
+            \result;
     assigns __fc_fds_state \from __fc_fds_state;
-    assigns readfds ≡ \null? \empty: *readfds
+    assigns *readfds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns writefds ≡ \null? \empty: *writefds
+    assigns *writefds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns errorfds ≡ \null? \empty: *errorfds
+    assigns *errorfds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns timeout ≡ \null? \empty: *timeout
+    assigns *timeout
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
@@ -7129,11 +7123,11 @@ extern int __va_ioctl_void(int fd, int request);
  */
 extern int __va_ioctl_int(int fd, int request, int arg);
 
-/*@ assigns \result, argp ≢ \null? *((char *)argp + (0 ..)): \empty;
+/*@ assigns \result, *((char *)argp + (0 ..));
     assigns \result
       \from (indirect: fd), (indirect: request),
             (indirect: *((char *)argp + (0 ..)));
-    assigns argp ≢ \null? *((char *)argp + (0 ..)): \empty
+    assigns *((char *)argp + (0 ..))
       \from (indirect: fd), (indirect: request), *((char *)argp + (0 ..));
  */
 extern int __va_ioctl_ptr(int fd, int request, void *argp);
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 42c80f2642d6fdde9b66d2ab9487b73f4ff7b8a8..9d071e5884c3e373da23a02893036f0d8bbbaee3 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -83,6 +83,8 @@
   function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
 [eva] tests/libc/signal_h.c:35: 
   function sigprocmask: precondition 'separation' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:35: 
+  Completely invalid destination for assigns clause *oldset. Ignoring.
 [eva] Done for function sigprocmask
 [eva] computing for function sigprocmask <- main.
   Called from tests/libc/signal_h.c:38.
@@ -137,6 +139,8 @@
   function sigaction: precondition 'valid_read_act_or_null' got status valid.
 [eva] tests/libc/signal_h.c:51: 
   function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:51: 
+  Completely invalid destination for assigns clause *oldact. Ignoring.
 [eva] Done for function sigaction
 [eva] Recording results for main
 [eva] done for function main
@@ -176,9 +180,7 @@
                 [15]{.sa_handler; .sa_sigaction} ∈ {0}
                 [15]{.sa_mask; .sa_flags} ∈ [--..--]
                 [16]{.sa_handler; .sa_sigaction} ∈ {0}
-                [16]{.sa_mask; .sa_flags} ∈ [--..--]
-                [17]{.sa_handler; .sa_sigaction} ∈ {0}
-                [17]{.sa_mask; .sa_flags} ∈ [--..--]
+                {[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
                 [18] ∈
                 {{ garbled mix of &{__fc_sigaction}
                  (origin: Library function) }}
diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle
index 41fa7f4bc4969060e4bf3300451702b172018a50..453a3465161df7694e3616278d3db5120e82a673 100644
--- a/tests/libc/oracle/sys_select.res.oracle
+++ b/tests/libc/oracle/sys_select.res.oracle
@@ -72,6 +72,10 @@
   function select: precondition 'errorfds' got status valid.
 [eva] tests/libc/sys_select.c:31: 
   function select: precondition 'timeout' got status valid.
+[eva:invalid-assigns] tests/libc/sys_select.c:31: 
+  Completely invalid destination for assigns clause *writefds. Ignoring.
+[eva:invalid-assigns] tests/libc/sys_select.c:31: 
+  Completely invalid destination for assigns clause *errorfds. Ignoring.
 [eva] Done for function select
 [eva] computing for function FD_ISSET <- main.
   Called from tests/libc/sys_select.c:32.
diff --git a/tests/libc/oracle/sys_time.res.oracle b/tests/libc/oracle/sys_time.res.oracle
index 3c7c79cab30db005eb3c7f1d6087a189d033aa56..18c18fa9f8cf4ac0e2cd2252f3a3baf3d7dcd62c 100644
--- a/tests/libc/oracle/sys_time.res.oracle
+++ b/tests/libc/oracle/sys_time.res.oracle
@@ -11,6 +11,8 @@
   function setitimer: precondition 'valid_new_value' got status valid.
 [eva] tests/libc/sys_time.c:6: 
   function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva:invalid-assigns] tests/libc/sys_time.c:6: 
+  Completely invalid destination for assigns clause *old_value. Ignoring.
 [eva] Done for function setitimer
 [eva] tests/libc/sys_time.c:7: assertion got status valid.
 [eva] computing for function setitimer <- main.
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index 5fcd6c6d027bc01e634adfc623934e6e724e7607..7e8f729d1beae0a1300355d51b3f1c84f7826b6c 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -37,9 +37,13 @@
   function nanosleep: precondition 'valid_nanosecs' got status valid.
 [eva] tests/libc/time_h.c:22: 
   function nanosleep: precondition 'valid_remaining_or_null' got status valid.
+[eva:invalid-assigns] tests/libc/time_h.c:22: 
+  Completely invalid destination for assigns clause *rmtp. Ignoring.
 [eva] Done for function nanosleep
 [eva] computing for function nanosleep <- main.
   Called from tests/libc/time_h.c:22.
+[eva:invalid-assigns] tests/libc/time_h.c:22: 
+  Completely invalid destination for assigns clause *rmtp. Ignoring.
 [eva] Done for function nanosleep
 [eva] computing for function clock_nanosleep <- main.
   Called from tests/libc/time_h.c:28.