[Inout] Fixes the location computed for \exit_status in assigns clauses.

Handles \exit_status exactly as \result.

src/plugins/inout/operational_inputs.ml

@@ -115,20 +115,21 @@ let eval_assigns kf state assigns =
                not (Kernel_function.is_formal v kf)
            | Base.CLogic_Var _ | Base.Null | Base.String _ -> true)
     in
+    let out_term = out.it_content in
     let outputs_under, outputs_over, deps =
       try
-        if Logic_utils.is_result out.it_content
+        if Logic_const.(is_result out_term || is_exit_status out_term)
         then (Zone.bottom, Zone.bottom, Zone.bottom)
         else
           let loc_out_under, loc_out_over, deps =
-	    !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out.it_content
+	    !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out_term
           in
 	  (enumerate_valid_bits_under Write loc_out_under,
 	   enumerate_valid_bits Write loc_out_over,
 	   clean_deps deps)
       with Db.Properties.Interp.No_conversion ->
         Inout_parameters.warning ~current:true ~once:true
-          "failed to interpret assigns clause '%a'" Printer.pp_term out.it_content;
+          "failed to interpret assigns clause '%a'" Printer.pp_term out_term;
         (Zone.bottom, Zone.top, Zone.top)
     in
     (* Compute all inputs as a zone *)

tests/spec/oracle/assigns_result.res.oracle

@@ -11,8 +11,6 @@
 [eva] Done for function f
 [eva] computing for function g <- main.
   Called from tests/spec/assigns_result.i:16.
-[inout] tests/spec/assigns_result.i:16: Warning: 
-  failed to interpret assigns clause '\exit_status'
 [eva] using specification for function g
 [eva] tests/spec/assigns_result.i:16: Warning: 
   cannot interpret assigns clause \exit_status