[Eva] Fixes API results on functions interpreted by a builtin or a specification.

Returns `Bottom instead of `Top at any statement of such functions.
In particular, [is_reachable stmt] is false for these statements.

src/plugins/value/engine/analysis.ml

@@ -100,8 +100,8 @@ module Make (Abstract: Abstractions.S) = struct
     then
       let kf = Kernel_function.find_englobing_kf stmt in
       match status kf with
-      | Unreachable -> `Bottom
-      | Analyzed NoResults | SpecUsed | Builtin _ -> `Top
+      | Unreachable | SpecUsed | Builtin _ -> `Bottom
+      | Analyzed NoResults -> `Top
       | Analyzed (Complete | Partial) -> f stmt
     else `Top
 

src/plugins/value/engine/analysis.mli

@@ -128,11 +128,11 @@ type status =
   | SpecUsed
   (** The function specification has been used to interpret its calls:
       its body has not been analyzed. Any request at a statement of this
-      function will lead to a Top result. *)
+      function will lead to a Bottom result. *)
   | Builtin of string
   (** The builtin of the given name has been used to interpret the function:
       its body has not been analyzed. Any request at a statement of this
-      function will lead to a Top result. *)
+      function will lead to a Bottom result. *)
   | Analyzed of results
   (** The function body has been analyzed. *)
 

src/plugins/value/utils/results.mli

@@ -60,7 +60,7 @@
     - the function has not been reached by the analysis: all requests in the
       function will lead to a Bottom error.
     - a specification or a builtin has been used instead of analyzing the
-      function body: all requests in the function will lead to a Top error.
+      function body: all requests in the function will lead to a Bottom error.
     - results have not been saved, due to the [-eva-no-results] parameter:
       all requests in the function will lead to a Top error. *)
 val are_available: Cil_types.kernel_function -> bool