diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml index 32b0492f4fe6badb5820c02e145c45ec53cc3f41..119668f8d36df7f5ae771562d120ff6693fe842a 100644 --- a/src/kernel_internals/typing/populate_spec.ml +++ b/src/kernel_internals/typing/populate_spec.ml @@ -354,9 +354,8 @@ struct else WritesAny let frama_c_default kf = - if Kernel_function.has_definition kf then - acsl_default () (* TODO: use genassigns *) - else Writes (Infer_annotations.assigns_from_prototype kf) + (* TODO: use genassigns for Definitions. *) + Writes (Infer_annotations.assigns_from_prototype kf) let compare_deps d1 d2 = match d1, d2 with