Frama-C Bug Tracking System - Frama-C
View Issue Details
0002201Frama-CPlug-in > wppublic2016-01-22 12:292016-06-21 14:08
rcl 
correnson 
normalminoralways
closedfixed 
LinuxUbuntu14.04
Frama-C Sodium 
Frama-C Aluminium 
0002201: Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))
With the help of a custom csmith variant, a program was discovered that causes an unexpected error in the wp plugin. The following program is a reduced minimal example of the failing program discovered by csmith: /*@ assigns \nothing; */ int main() { int foo = 1; 1 & (foo & 0x80000000000001LL) << 1; return 0; } The crash message is: Raised at file "src/wp/register.ml", line 579, characters 30-32 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 763, characters 2-9 Called from file "src/kernel/cmdline.ml", line 216, characters 4-8 Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Sodium-20150201.
Save the aforementioned program into a file named test.c, then execute frama-c -wp test.c to cause the crash.
No tags attached.
c test.c (103) 2016-01-22 12:29
https://bts.frama-c.com/file_download.php?file_id=1079&type=bug
Issue History
2016-01-22 12:29rclNew Issue
2016-01-22 12:29rclStatusnew => assigned
2016-01-22 12:29rclAssigned To => correnson
2016-01-22 12:29rclFile Added: test.c
2016-01-25 09:38corrensonAssigned Tocorrenson => patrick
2016-01-26 11:16patrickStatusassigned => confirmed
2016-01-26 12:07corrensonNote Added: 0006123
2016-01-26 12:07corrensonAssigned Topatrick => correnson
2016-01-26 12:07corrensonStatusconfirmed => resolved
2016-01-26 12:07corrensonResolutionopen => fixed
2016-06-21 14:08signolesFixed in Version => Frama-C Aluminium
2016-06-21 14:08signolesStatusresolved => closed

Notes
(0006123)
correnson   
2016-01-26 12:07   
Fix committed to master branch.