diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml index 2046b2b4bed3954cd134ae8cf36ec5864bb8c7c3..d337b04075cf4cf072e9d28ed1d371341bd7f76a 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml @@ -57,7 +57,7 @@ let pre_funspec kf kinstr env funspec = unsupported (fun spec -> let ppt = Property.ip_decreases_of_spec kf kinstr spec in - if must_translate_opt ppt then Env.not_yet env "variant clause") + if must_translate_opt ppt then Env.not_yet env "decreases clause") funspec; (* TODO: spec.spec_terminates is not part of the E-ACSL subset *) unsupported