Merge branch 'feature/wp/fix-lambda' into 'master'

[wp] fix error message with eta-expansion

See merge request frama-c/frama-c!2415

src/plugins/wp/LogicCompiler.ml

@@ -878,14 +878,18 @@ struct
         | LFUN phi -> e_fun phi [] ~result:(Lang.tau_of_ltype x.lv_type)
       in Cvalues.plain x.lv_type v
     with Not_found ->
-      Wp_parameters.fatal "Unbound logic variable '%a'"
-        Printer.pp_logic_var x
+      if Logic_env.is_logic_function x.lv_name then
+        Warning.error "Lambda-functions not yet implemented (at '%s')"
+          x.lv_name
+      else
+        Wp_parameters.fatal "Name '%a' has no definition in term"
+          Printer.pp_logic_var x
 
   let logic_info env f =
     try
       match Logic_var.Map.find f.l_var_info env.vars with
       | Vexp p -> Some (F.p_bool p)
-      | _ -> Wp_parameters.fatal "Logic variable '%a' is not a predicate"
+      | _ -> Wp_parameters.fatal "Variable '%a' is not a predicate"
                Logic_info.pretty f
     with Not_found -> None