GitLab

ID0000701: This issue was created automatically from Mantis Issue 701. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000701	Frama-C	Plug-in > wp	public	2011-02-02	2011-04-13

Reporter	regehr	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101202-beta2	Target Version	-	Fixed in Version	Frama-C Carbon-20110201

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); }