Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001332Frama-CPlug-in > wppublic2012-12-15 21:392012-12-15 21:39
ReporterPhilippe 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001332: [wp] failure: not an integer (Blob)
Description> cat bar.c
typedef struct S { signed char x[16]; } S;

/*@ axiomatic Y { logic integer Z (S t, integer i, integer j) reads t.x[i..j]; } */

/*@ ensures \result == Z(s, 0, 15); */
int foo(S s) { return 0; }

> frama-c -wp -wp-rte -wp-fct foo bar.c
[kernel] preprocessing with "gcc -C -E -I. bar.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] warning: Interpreting reads-definition as expressions rather than tsets
bar.c:6:[wp] failure: not an integer (Blob)
[kernel] The full backtrace is:
         Raised at file "src/kernel/log.ml", line 523, characters 30-31
         Called from file "src/kernel/log.ml", line 517, characters 9-16
         Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
         Called from file "src/wp/translate_prop.ml", line 911, characters 16-71
         Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
         Called from file "src/wp/translate_prop.ml", line 1579, characters 32-52
         Called from file "list.ml", line 69, characters 12-15
         Called from file "src/wp/translate_prop.ml", line 1974, characters 14-68
         Re-raised at file "src/wp/translate_prop.ml", line 2029, characters 12-15
         Called from file "src/wp/translate_prop.ml", line 1827, characters 27-34
         Re-raised at file "src/wp/translate_prop.ml", line 1831, characters 43-48
         Called from file "src/wp/translate_prop.ml", line 2188, characters 21-56
         Called from file "src/wp/translate_prop.ml", line 1570, characters 17-59
         Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
         Called from file "src/wp/translate_prop.ml", line 1745, characters 19-38
         Called from file "src/wp/translate_prop.ml", line 1707, characters 13-30
         Called from file "src/wp/wp_error.ml", line 102, characters 13-20
         Re-raised at file "src/wp/wp_error.ml", line 95, characters 20-23
         Called from file "src/wp/cfgWeakestPrecondition.ml", line 224, characters 17-33
         Called from file "src/wp/cfgWeakestPrecondition.ml", line 154, characters 18-44
         Re-raised at file "src/wp/wp_error.ml", line 90, characters 20-23
         Called from file "src/wp/cfgWeakestPrecondition.ml", line 165, characters 34-54
         Re-raised at file "src/wp/cfgWeakestPrecondition.ml", line 184, characters 14-17
         Called from file "src/wp/cfgpropid.ml", line 96, characters 10-20
         Re-raised at file "src/wp/cfgpropid.ml", line 100, characters 14-15
         Called from file "src/wp/cfgpropid.ml", line 140, characters 12-59
         Called from file "list.ml", line 74, characters 24-34
         Called from file "src/wp/calculus.ml", line 326, characters 22-64
         Called from file "src/wp/calculus.ml", line 336, characters 23-45
         Called from file "src/wp/calculus.ml", line 575, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 548, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 551, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 551, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 541, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 536, characters 20-43
         Called from file "src/wp/calculus.ml", line 498, characters 21-42
         Called from file "src/wp/calculus.ml", line 661, characters 40-59
         Called from file "set.ml", line 288, characters 38-41
         Called from file "set.ml", line 293, characters 37-58
         Called from file "set.ml", line 293, characters 42-57
         Called from file "set.ml", line 293, characters 42-57
         Called from file "src/wp/calculus.ml", line 661, characters 4-64
         Called from file "src/wp/calculus.ml", line 708, characters 19-51
         Called from file "src/wp/cfgProof.ml", line 238, characters 30-53
         Called from file "list.ml", line 69, characters 12-15
         Called from file "src/wp/cfgProof.ml", line 228, characters 8-666
         Called from file "src/wp/register.ml", line 586, characters 22-41
         Called from file "src/wp/register.ml", line 679, characters 17-24
         Re-raised at file "src/wp/register.ml", line 683, characters 32-34
         Called from file "src/wp/register.ml", line 678, characters 17-24
         Re-raised at file "src/wp/register.ml", line 682, characters 29-31
         Called from file "src/wp/register.ml", line 678, characters 17-24
         Re-raised at file "src/wp/register.ml", line 682, characters 29-31
         Called from file "src/wp/register.ml", line 678, characters 17-24
         Re-raised at file "src/wp/register.ml", line 682, characters 29-31
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 38, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
         Plug-in wp aborted: internal error.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-12-15 21:39 Philippe New Issue
2012-12-15 21:39 Philippe Status new => assigned
2012-12-15 21:39 Philippe Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker