0000701: Unexpected error (Failure("int_of_string")).

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

Relationships

Notes
(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.

Issue History
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