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.