ID0002023: **This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002023 | Frama-Clang | Documentation > ACSL | public | 2014-12-08 | 2015-02-16 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open | | **Priority** | normal | **Severity** | text | **Reproducibility** | always | | **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : For the assertion in line 3 of the attached file "198.c", Frama-c generates the following proof obligation for Alt-Ergo: "goal foo_assert: forall i : int. is_uint32(i) -> ((-1) = i)". However, axiom "is_uint32_def" in line 430 of file "foo_assert_Alt-Ergo.mlw" says: "is_uint32(x) -> (0 <= x)", while "0 <= -1" is false (and unprovable as an own goal by Alt-Ergo). As a consequence, there exists no (satisfiable) precondition "requires p(i)" that could be added as contract of "foo()" such that the assertion in line 3 becomes satisfiable, since "forall i : int. p(i) -> is_uint32(i) -> ((-1) = i)" implies "forall i : int. p(i) -> is_uint32(-1)". For example, requiring "i == 0xffffffffu" doesn't make line 3 provable, nor does any similar equation. ## Attachments - [198.c](/uploads/43894779f84ecb85c5bbca9c5d4f60c5/198.c) - [foo_assert_Alt-Ergo.mlw](/uploads/2d9028c59b5be767e57c7919eccb4d8b/foo_assert_Alt-Ergo.mlw) - [198a.c](/uploads/387d28aa89210ab23bd7de97f80871b9/198a.c) - [2compl.txt](/uploads/5886d302a5d8d0deae8deb56309ab3fe/2compl.txt)