False valid with LONG_MIN
ID0002088: This issue was created automatically from Mantis Issue 2088. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002088 | Frama-C | Plug-in > wp | public | 2015-03-06 | 2015-03-09 |
| Reporter | Ian | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Ubuntu | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
A pre-condition is being incorrectly validated when LONG_MIN is passed. I am in a 64bit environment.
Steps To Reproduce :
long_precondition.c: #include <limits.h> /*@ requires i == 0; assigns \nothing; */ extern void foo(long i); void bar() { foo(LONG_MIN); }
Run command: frama-c long_precondition.c -wp -pp-annot
Output received: [kernel] preprocessing with "gcc -C -E -I. -dD long_precondition.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_bar_call_foo_pre : Valid [wp] Proved goals: 1 / 1 Qed: 1
Output expected: Unknown for goal typed_bar_call-foo_pre
Note: This behavior is still observed if the option -pp-annot is removed, and INT_MIN is replaced by its expansion "-9223372036854775807L - 1L"