WP: internal error: only the kernel should set the status of property assumes
ID0002383: This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
Reporter | evdenis | Assigned To | correnson | Resolution | unable to reproduce |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | - | Target Version | - | Fixed in Version | Frama-C 17-Chlorine |
Description :
Example:
int test(void) { int a = 1; /*@ behavior ok: assumes a > 0; ensures \true; */ return 3; }
Command:
frama-c -wp test.c
Log:
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable) [wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable) [kernel] failure: only the kernel should set the status of property assumes a > 0 [kernel] Current source was: test.c:1 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16 Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109 Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80 Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71 Called from file "list.ml", line 85, characters 12-15 Called from file "list.ml", line 85, characters 12-15 Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38 Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28 Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68 Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67 Called from file "map.ml", line 270, characters 20-25 Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39 Called from file "src/plugins/wp/register.ml", line 654, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8 Frama-C aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/.