diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml index 3df4c0086321b7029848e3f25d6b536634a12e38..ea48d5ad04b302cde1962649b6154f0c8b2e16db 100644 --- a/src/plugins/inout/operational_inputs.ml +++ b/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 *) diff --git a/tests/spec/oracle/assigns_result.res.oracle b/tests/spec/oracle/assigns_result.res.oracle index be625108d0cc0a76d746cf2a203d0f00b79b70d4..f492644ff778a0fd8afe7cbcf2d9cd7cf94f4062 100644 --- a/tests/spec/oracle/assigns_result.res.oracle +++ b/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