| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 21:15 | 2019-10-17 17:59 | ||||
| Reporter | hugo.gimbert | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | won't fix | ||||||
| Platform | macosx | OS | mojave | OS Version | 10.14.1 | ||||
| Product Version | Frama-C 17-Chlorine | ||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0002409: crash | ||||||||
| Description | frama-c -wp somme.c with somme.c containing /*@ logic integer f(integer k) = k; lemma sumint: \forall int n; n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2; */ leads to crash Trace below | ||||||||
| Additional Information | [kernel] Parsing somme.c (with preprocessing) [wp] Failure: Unbound logic variable 'f' [kernel] Current source was: somme.c:4 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16 Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38 Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32 Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35 Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23 Called from file "list.ml", line 88, characters 20-23 Called from file "list.ml", line 88, characters 32-39 Called from file "list.ml", line 88, characters 32-39 Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32 Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35 Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23 Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42 Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51 Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42 Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46 Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60 Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104 Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46 Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42 Called from file "map.ml", line 295, characters 20-25 Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47 Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45 Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36 Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202 Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20 Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28 Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36 Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023 Called from file "src/plugins/wp/register.ml", line 689, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48 Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 791, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8 Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Chlorine-20180502. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines hugo-9:TP3 gimbert$ cat somme.c /*@ logic integer f(integer k) = k; lemma sumint: \forall int n; n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2; */ | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |  somme.c [^] (111 bytes) 2018-11-13 21:15 [Show Content]
| ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0006677) correnson (manager) 2018-11-14 09:18 |
ACSL \sum construct is not supported by WP. Sorry. You shall axiomatise the definition via a dedicated logic function, say sum_f(n), with sum_f(0) = 0 and sum_f(k+1) = sum_f(k) + f(k) for k>=0. |
|
(0006678) correnson (manager) 2018-11-14 09:19 |
\sum not supported, workaround proposed. |
|
(0006683) signoles (manager) 2018-11-30 10:06 |
Would be solved only when WP would not crash, but generate a gentle error message instead. |
|
(0006899) correnson (manager) 2019-10-17 16:37 |
The problem is **not** the \sum but the fact that `f` is not a variable but a function. By replacing \sum(0,n,f) with \sum(0,n,\lambda integer x;f(x)) we obtain a more clever message : [wp] /Users/correnson/Downloads/somme.c:5: User Error: Lambda-functions not yet implemented I will fix the WP lookup function that will accept a function name instead of its eta-expanded lambda representation. |
|
(0006901) correnson (manager) 2019-10-17 16:59 |
Gentler error message in development version. Although, lambda functions and \sum are not yet implemented in Frama-C. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2018-11-13 21:15 | hugo.gimbert | New Issue | |
| 2018-11-13 21:15 | hugo.gimbert | Status | new => assigned |
| 2018-11-13 21:15 | hugo.gimbert | Assigned To | => correnson |
| 2018-11-13 21:15 | hugo.gimbert | File Added: somme.c | |
| 2018-11-14 09:18 | correnson | Note Added: 0006677 | |
| 2018-11-14 09:19 | correnson | Note Added: 0006678 | |
| 2018-11-14 09:19 | correnson | Status | assigned => resolved |
| 2018-11-14 09:19 | correnson | Resolution | open => not fixable |
| 2018-11-30 10:06 | signoles | Note Added: 0006683 | |
| 2018-11-30 10:06 | signoles | Status | resolved => confirmed |
| 2019-10-17 16:37 | correnson | Note Added: 0006899 | |
| 2019-10-17 16:59 | correnson | Note Added: 0006901 | |
| 2019-10-17 16:59 | correnson | Status | confirmed => resolved |
| 2019-10-17 16:59 | correnson | Resolution | not fixable => won't fix |
| 2019-10-17 17:59 | signoles | Status | resolved => closed |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|