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