Anonymous | Login | Signup for a new account | 2019-02-17 03:55 CET | ![]() |
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 | ||||
0000701 | Frama-C | Plug-in > wp | public | 2011-02-02 05:44 | 2011-04-13 15:28 | ||||
Reporter | regehr | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C Carbon-20101202-beta2 | ||||||||
Target Version | Fixed in Version | Frama-C Carbon-20110201 | |||||||
Summary | 0000701: Unexpected error (Failure("int_of_string")). | ||||||||
Description | Seen on Ubuntu 10.10 on x86. OCaml and related packages are all from Ubuntu, I don't think I've customized anything in particular on this machine. regehr@home:~/csmith/runtime$ frama-c -wp -wp-rte add.c [kernel] preprocessing with "gcc -C -E -I. add.c" [rte] annotating function safe_add [rte] annotating function unsafe_add [kernel] The full backtrace is: Raised at file "src/kernel/command.ml", line 42, characters 10-13 Called from file "src/wp/cfgProof.ml", line 125, characters 4-118 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "list.ml", line 69, characters 12-15 Called from file "src/wp/cfgProof.ml", line 223, characters 1-607 Called from file "src/wp/register.ml", line 322, characters 41-57 Called from file "src/wp/register.ml", line 464, characters 3-32 Called from file "src/wp/register.ml", line 533, characters 8-20 Called from file "src/wp/register.ml", line 570, characters 4-18 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 660, characters 2-9 Called from file "src/kernel/cmdline.ml", line 173, characters 4-8 Unexpected error (Failure("int_of_string")). Please report as 'crash' at http://bts.frama-c.com/ [^] Note that a backtrace alone often does not have 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 [^] regehr@home:~/csmith/runtime$ cat add.c int unsafe_add (int a, int b) { return a+b; } int safe_add (int si1, int si2) { return (((si1>0) && (si2>0) && (si1 > ((2147483647)-si2))) || ((si1<0) && (si2<0) && (si1 < ((-2147483647-1)-si2)))) ? ((si1)) : (si1 + si2); } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | |||||||||
![]() |
|
(0001457) correnson (manager) 2011-02-02 13:27 |
Since revision R11167. |
(0001756) signoles (manager) 2011-04-13 15:28 |
Fixed in WP 0.3 compatible with Frama-C Carbon. |
![]() |
|||
Date Modified | Username | Field | Change |
2011-02-02 05:44 | regehr | New Issue | |
2011-02-02 05:44 | regehr | Status | new => assigned |
2011-02-02 05:44 | regehr | Assigned To | => dargaye |
2011-02-02 06:27 | signoles | Assigned To | dargaye => correnson |
2011-02-02 13:27 | correnson | Note Added: 0001457 | |
2011-02-02 13:27 | correnson | Status | assigned => resolved |
2011-02-02 13:27 | correnson | Fixed in Version | => Frama-C Carbon-20110201 |
2011-02-02 13:27 | correnson | Resolution | open => fixed |
2011-04-13 15:28 | signoles | Note Added: 0001756 | |
2011-04-13 15:28 | signoles | Status | resolved => closed |
Copyright © 2000 - 2019 MantisBT Team |