diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml index f5fec8bab83864cb5d53747825af69ce0daec23c..a422d2d46d3b234e68adf1b58500ce4067bc9b3b 100644 --- a/src/plugins/eva/domains/octagons.ml +++ b/src/plugins/eva/domains/octagons.ml @@ -1811,7 +1811,6 @@ module Domain = struct state >>-: check "precise assign" let assign kinstr left_value expr assigned valuation state = - update valuation state >>- fun state -> if kinstr <> Kglobal && Cil.isIntegralOrPointerType left_value.ltyp && not (Eval_typ.lval_contains_volatile left_value.lval)