misc/coverity_model.c
author nemo
Mon, 11 May 2015 13:53:08 -0400
changeset 10942 5d7dd938dedc
parent 10498 bcd1d7ad2f3e
permissions -rw-r--r--
This probably fixes bug #839 - mine time was hardcoded to 3000 in Attack, instead of using the "0 as undefined" input that other places were using. When re653e96b0ec3 started paying attention to the input parameter, this previously ignored value became a problem.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10498
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     1
void fpcrtl_halt(int num) {
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     2
    __coverity_panic__();
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     3
}
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     4
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     5
int fpcrtl_abs(int num) {
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     6
    return num >= 0 ? num : -num;
bcd1d7ad2f3e Model file for coverity checks
unc0rr
parents:
diff changeset
     7
}