bitwise negation of uint introduces "-1" in Alt-Ergo obligation
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.