0002409: crash - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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

/*@
logic integer f(integer k) = k;

lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
 */

somme.c (111 bytes) 2018-11-13 21:15

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

Date Modified	Username	Field	Change
Issue History
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