diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml index 882e9a63c23a6ced23e34a1659c72bf432903e9d..478be2e40ea72324d85484a651060284bec8d474 100644 --- a/src/plugins/reduc/hyp.ml +++ b/src/plugins/reduc/hyp.ml @@ -20,9 +20,9 @@ (* *) (**************************************************************************) -let pred_opt_from_expr_state state e = +let pred_opt_from_expr_state stmt e = try - Value2acsl.lval_to_predicate state e + Value2acsl.lval_to_predicate stmt e with | Cvalue.V.Not_based_on_null -> Misc.not_implemented ~what:"Value not based on null"; diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli index 4d1aacea7b09d36abda69936d9016a77a3150b6a..e69aca30b89ac9004dd0ffb548e7ec90d547b8a2 100644 --- a/src/plugins/reduc/value2acsl.mli +++ b/src/plugins/reduc/value2acsl.mli @@ -27,5 +27,5 @@ open Cil_types @return None if no such predicate can be created. *) val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option -val lval_to_predicate: ?loc:location -> Cil_types.stmt -> lval -> predicate option -val exp_to_predicate: ?loc:location -> Cil_types.stmt -> exp -> predicate option +val lval_to_predicate: ?loc:location -> stmt -> lval -> predicate option +val exp_to_predicate: ?loc:location -> stmt -> exp -> predicate option