diff --git a/.Makefile.lint b/.Makefile.lint index cdddb760969cc6f1075006562db65d2c0cc5af02..fc916bfa1e33d42ff2e73b588b496e21b2d85da4 100644 --- a/.Makefile.lint +++ b/.Makefile.lint @@ -23,8 +23,6 @@ ML_LINT_KO+=src/kernel_internals/typing/mergecil.ml ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli ML_LINT_KO+=src/kernel_internals/typing/oneret.ml ML_LINT_KO+=src/kernel_internals/typing/oneret.mli -ML_LINT_KO+=src/kernel_internals/typing/rmtmps.ml -ML_LINT_KO+=src/kernel_internals/typing/rmtmps.mli ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.ml ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.mli ML_LINT_KO+=src/kernel_internals/typing/unroll_loops.ml diff --git a/src/kernel_internals/typing/rmtmps.mli b/src/kernel_internals/typing/rmtmps.mli index 61f496354236aac967e2bd4862dc037fd4248b72..510a6565b0551e9045c09aa3913ec2d8735dd80d 100644 --- a/src/kernel_internals/typing/rmtmps.mli +++ b/src/kernel_internals/typing/rmtmps.mli @@ -72,7 +72,7 @@ * Note that certain CIL- and CCured-specific pragmas induce * additional global roots. This functionality is always present, and * is not subject to replacement by "filterRoots". - *) +*) type rootsFilter = Cil_types.global -> bool @@ -83,10 +83,10 @@ val isCompleteProgramRoot : rootsFilter val removeUnusedTemps: ?isRoot:rootsFilter -> Cil_types.file -> unit (** removes unused labels for which [is_removable] is true. -[is_removable] defaults to the negation of boolean flag of [Label] -{i i.e.} only labels generated by CIL may be removed. -@since Carbon-20101201 - *) + [is_removable] defaults to the negation of boolean flag of [Label] + {i i.e.} only labels generated by CIL may be removed. + @since Carbon-20101201 +*) val remove_unused_labels: ?is_removable:(Cil_types.label -> bool) -> Cil_types.fundec -> unit