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))

Yes, the version nicknamed “Boron” is quite old. It is the newest version for which a Windows binary is available on http://frama-c.com/ . That may be why you are using it. Have you tried the instructions written by Stéphane Duprat (http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-February/003040.html ) to gain two versions? — Pascal Cuoq, Jul 31 '13 at 11:01
@pascal-cuoq, I do now, thanks, and am now working with WP. In case other folks find this, alt-ergo-0.94-mingw.exe seems to be required. The Nitrogen-over-Boron instructions point to it but don't seem to require it. To install: download it, rename to alt-ergo.exe, and put it somewhere in your PATH ahead of Boron's bin. I avoided alt-ergo-0.95-mingw.exe because its site says it's incompatible with Frama-C-Oxygen and 0.94 is known to work with -Nitrogen. Also: follow that link's instructions to set all three FRAMAC_* env. vars; the INSTALL.txt only mentions one. Thanks! — Barrie Slaymaker, Jul 31 '13 at 17:28

score 2 · Accepted Answer · answered Jul 31 '13 at 09:34

2

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.

answered Jul 31 '13 at 09:34

Virgile

9,724
18
42

thanks--very informative! How does that (contradictory) hypothesis allow alt-ergo to prove that integer_of_32(return) == 2147483647? For example, does a contradiction like this allow alt-ergo prove all hypotheses, or is alt-ergo finding a proof because forall result:int32 (for example) only ranges over int32? The proof steps in gWhy (sorry--gWhy won't let me copy to clipboard) go through the hypothesis you mention (H8, here) and then through the __retres and return hypotheses. – Barrie Slaymaker Jul 31 '13 at 15:03
It's not just alt-ergo. Basically, as soon as you have two contradictory hypotheses in your context, you can prove anything. This is a very old logic rule, so old in fact that it has a latin name: _Ex falso quod libet_ (from the false [deduce] what you want). – Virgile Aug 01 '13 at 07:06
How do we know that there are a complete set of safety POs (RTE POs, in WP, now that I'm using Flourine) generated, so that at least one will always fail in cases like this, where contradictory hypotheses generated by Frama-C enable false proofs? I assume that it's not possible, or at least feasible, to prevent Frama-C from generating contradictory hypotheses from non-contradictory specification POs. – Barrie Slaymaker Aug 02 '13 at 13:29
Well, there is no definitive answer to this. The RTE plugin is supposed to generate alarms for all possible run-time errors, but I don't have a formal proof of that. Also RTE does not generate contradictory hypotheses. It can generate assertions that are contradictory to the assumption that the program is exempt from run-time errors, but that precisely its purpose. – Virgile Aug 08 '13 at 09:49

ensures proved even though code is defective?

1 Answers1