diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml index 58954c2c2d50aa4fb430dd73db2d4eb78f253c1a..c7bc16170556849f5fde164bb3e8e0374be3e952 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/src/plugins/e-acsl/typing.ml @@ -540,7 +540,6 @@ let get_op t = extract_typ t info.op let get_cast t = - Cil.CurrentLoc.set t.term_loc; let info = Memo.get t in try Extlib.opt_map typ_of_integer_ty info.cast with Not_an_integer -> None diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli index 2d90b0ec691900c5d33cdef404ce0e98348a76f5..246847c903f356c60032c033fd40239c3d91d6ce 100644 --- a/src/plugins/e-acsl/typing.mli +++ b/src/plugins/e-acsl/typing.mli @@ -35,8 +35,6 @@ type integer_ty = private | C_type of ikind | Other -include Datatype.S with type t = integer_ty - val gmp: integer_ty val c_int: integer_ty val ikind: ikind -> integer_ty