ID0001332: **This issue was created automatically from Mantis Issue 1332. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001332 | Frama-C | Plug-in > wp | public | 2012-12-15 | 2012-12-15 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Philippe | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | crash | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - | ### 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.