Bug#498485: why: calls cpulimit with wrong arguments

[Timo Juhani Lindfors <timo.lindfors@iki.fi>]

Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr> writes:
> Timo Juhani Lindfors a écrit :
>> Package: why
>> Version: 1.13-1
>> Severity: normal
>> 
>> calldp.ml calls cpulimit with
>> 
>
>>From 2.01 (according to changelog[1]), Why started using its own version
> of cpulimit (why-cpulimit) and doesn't depend anymore on cpulimit
> (debian package).
>
> Now Why uses only why-cpulimit.
> So the bug disappeared with Why 2.01.
>
> Try to get a newer version of Why !

Whoops, I made a typo: I have why version "2.13-1" and not "1.13-1"
and I definitely can still see the bug:

Steps to reproduce:
0) cat > Lesson1.java <<EOF
public class Lesson1 {
    // jml2:
    // requires a != null && (\forall int i; 0 < i && i < a.length; a[i-1] <= a[i]);
    // krakatoa:
    //@ requires a != null && (\forall integer i; 0 < i && i < a.length ==>  a[i-1] <= a[i]);
    public int f0(int[] a) {
        return a[0];
    }
}
EOF
1) strace -o s -s4096 -f gwhy Lesson1.java
2) click ergo in the GUI

Expected results:
2) gwhy runs ergo

Actual results:
2) ergo is not started, strace reveals

852   execve("/usr/bin/cpulimit", ["cpulimit", "10", "ergo", "/tmp/gwhy9f0a8a_why.why"], [/* 46 vars */] <unfinished ...>

...

852   write(2, "Error: You must specify a target process\n"..., 41) = 41
852   write(2, "Usage: cpulimit TARGET [OPTIONS...]\n"..., 36) = 36
852   write(2, "   TARGET must be exactly one of these:\n"..., 40) = 40
852   write(2, "      -p, --pid=N        pid of the process\n"..., 44) = 44
852   write(2, "      -e, --exe=FILE     name of the executable program file\n"..., 61) = 61
852   write(2, "      -P, --path=PATH    absolute path name of the executable program file\n"..., 75) = 75
852   write(2, "   OPTIONS\n"..., 11)   = 11
852   write(2, "      -l, --limit=N      percentage of cpu allowed from 0 to 100 (mandatory)\n"..., 77) = 77
852   write(2, "      -v, --verbose      show control statistics\n"..., 49) = 49
852   write(2, "      -z, --lazy         exit if there is no suitable target process, or if it dies\n"..., 84) = 84
852   write(2, "      -h, --help         display this help and exit\n"..., 52) = 52

Please let me know if you are unable to reproduce this bug with 2.13-1.


best regards,
Timo Lindfors