ensures proved even though code is defective?

Question

In the following, how are the postconditions for behavior neg_limit being proven true when the relevant C code is commented-out?

One of the Safety->check arithmetic overflow isn't provable, as expected, but it seems like neg_limit should also be unprovable.

Context: I'm using Frama-C-Boron, Jessie and, via gWhy, Alt-Ergo in order to learn how to write specifications and prove that functions meet them. Any cluebatting, RTFMing, etc., about specification strategies, tools, etc. is also appreciated. So far, I am reading both the ACSL 1.7 implementation manual (which is more recent that -Boron's) and the Jessie tutorial & ref. manual.

Thanks!

/*@ behavior non_neg:
        assumes v >= 0;
        ensures \result == v;

    behavior neg_in_range:
        assumes INT32_MIN < v < 0;
        ensures \result == -v;

    behavior neg_limit:
        assumes v == INT32_MIN;
        ensures \result == INT32_MAX;

    disjoint behaviors;
    complete behaviors;
*/
int32_t my_abs32(int32_t v)
{
  if (v >= 0)
    return v;

  //if (v == INT32_MIN)
  //  return INT32_MAX;

  return -v;
}

Here is the gWhy goal for the first postcondition:

goal my_abs32_ensures_neg_limit_po_1:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) >= 0) ->
  forall __retres:int32.
  (__retres = v_2) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

and for the second:

goal my_abs32_ensures_neg_limit_po_2:
  forall v_2:int32.
  (integer_of_int32(v_2) = ((-2147483647) - 1)) ->
  (integer_of_int32(v_2) < 0) ->
  forall result:int32.
  (integer_of_int32(result) = (-integer_of_int32(v_2))) ->
  forall __retres:int32.
  (__retres = result) ->
  forall return:int32.
  (return = __retres) ->
  ("JC_13": (integer_of_int32(return) = 2147483647))

Answer 1

Regarding documentation, you might want to have a look at Fraunhofer FOKUS' ACSL By Example: http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

Concerning your question, I've repeated your result (BTW, you're missing an #include <stdint.h>" in your code) with Frama-C Fluorine, and Jessie+Alt-ergo still manages to prove the post-condition. But remember that the post-condition is proved under the hypothesis that no runtime error occurs, which is not the case of your code, as the failed safety PO shows.

Namely, the second post-condition contains the hypothesis (integer_of_int32(result) = (-integer_of_int32(v_2))) which can be rewritten as (integer_of_int32(result) = 2147483648). This is in contradiction with an axiom in Jessie's prelude, that says that forall v:int32. integer_of_int32(v)<=2147483647.

I guess that this outlines once again that you cannot claim to have verified an ACSL annotation as long as some proof obligations remain unchecked, even if they do not stem directly from this annotation.