Tuples are not supported
Error while using types and predicates with the WP plugin
Steps to reproduce the issue
Copy the code snippet from Example 2.35 in Section 2.5.3 in the latest ACSL manual (https://frama-c.com/download/frama-c-acsl-implementation.pdf) and run Frama-C on this code file, with the WP plugin.
Expected behaviour
Frama-C should not throw any errors and verify the given method using the predicate.
Actual behaviour
Multiple errors are reported as follows in the Kernel logs:
[kernel:annot-error] /code.c:4: Warning: unexpected token '('
[kernel:annot-error] /code.c:7: Warning: unexpected token '('
[kernel:annot-error] /code.c:16: Warning: unexpected token ','
which corresponds to the lines:
line 4: //@ type intpair = (integer,integer);
line 7: @ \let (x1,y1) = p1 ;
line 16: @ loop variant (x, y) for lexico;
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
Additional comments
I'm not sure what I'm missing here? Is there some flag I'm supposed to switch on, while using these features? Or use a different plugin?
Is there any other way of specifying lexicographically ordered terms as a variant in Frama-C?