Unable to call built-in ACSL pow function that takes integer arguments and returns an integer
Steps to reproduce the issue
/*@
assigns \nothing;
ensures 2 <= \result <= 4;
*/
int do_something(void) {
return 2;
}
/*@
assigns \nothing;
*/
int main(void) {
int foo = 8;
int bar = do_something();
int baz = 3;
// Unnatural whitespace so that
// the line number given by the error can be specific.
/*@ assert FooInequality: foo <= pow(
bar
,
baz
);
*/
return foo;
}
$ frama-c -wp -wp-rte main.c
Expected behaviour
The file is parsed successfully, and the goals may or may not be proved successfully.
Actual behaviour
$ frama-c -wp -wp-rte main.c
[kernel] Parsing main.c (with preprocessing)
[kernel:annot-error] main.c:21: Warning:
invalid implicit conversion from 'int' to 'double'. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "main.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
Page 100 of the ACSL v1.18 manual has appendix A.2 Builtin functions
listing integer pow(integer x, integer y) ;
I would expect parsing to succeed due to this.
However, that function is the only in the whole section to not start with a \
.
If we instead call \pow
, the parsing succeeds, but we can use frama-c-gui
to see that reals and not integers are involved in the unproven goal.
Adding (integer)
casts to bar
and baz
in the annotation does not cause an integer pow function to be used.
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, alt-ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
Additional information (optional)
Similar issue: #2506 (closed)