I would like to have a way to describe logic/spec level structs that include abstract lists. Example 2.2.7 on page 27 of the ACSL Reference Manual suggests that there is a way to do this and it is as follows:
//@ type point = struct { real x; real y; };
//@ type triangle = point[3];
//@ logic point origin = { .x = 0.0 , .y = 0.0 };
/*@ logic triangle t_iso = { [0] = origin,
@ [1] = { .y = 2.0 , .x = 0.0 }
@ [2] = { .x = 2.0 , .y = 0.0 }};
@*/
/*@ logic point centroid(triangle t) = {
@ .x = mean3(t[0].x,t[1].x,t[2].x);
@ .y = mean3(t[0].y,t[1].y,t[2].y);
@ };
@*/
//@ type polygon = point[];
/*@ logic perimeter(polygon p) =
@ \sum(0,\length(p)-1,\lambda integer i;d(p[i],p[(i+1) % \length(p)])) ;
@*/
If I copy/paste this exact code into a text editor and try to run this code with the wp plugin with:
frama-c -wp -wp-rte -wp-prover alt-ergo shapes.c
I get an error:
[kernel:annot-error] shapes.c:1: Warning: unexpected token '{'
If I give up on trying to write logic/spec level declarations of struct types, but would still like to write logic/spec level expressions that instantiate structs defined in C as follows:
struct somestruct {
int x;
int y;
};
/*@
logic struct somestruct foo = { .x = 3, .y = 4 };
*/
I still get an error:
[kernel:annot-error] aggregate_err.c:7: Warning:
unsupported aggregated field construct. Ignoring global annotation
and not having a way to write particular values of structs as expressions in specifications leads to some fairly ugly specifications, so I am hoping that I am doing something wrong.
If I dig into the source of frama-C 20.0 to try to find the part of the parser-generator code for /*@ type declarations, it looks like the syntax in Ex 2.2.7 is not really implemented. It looks like the syntax for type level declarations is line 799 of
frama-c-20.0-Calcium/src/kernel_internals/parsing/logic_parser.mly
(called type_spec)
And the parse rule for type level declarations of structs is:
| STRUCT exit_rt_type identifier_or_typename { LTstruct $3 }
which looks like it would support
//@ type foo = struct c_struct;
but not something like what Ex 2.2.7 has as in:
//@ type point = struct { real x; real y; };
Is there something else I should be doing to have better support for structs in ACSL/Frama-C? Thanks!
Not all ACSL constructions are supported by the current Frama-C implementation. With each Frama-C release comes an ACSL implementation manual, which describes the constructions that are not yet implemented. For Frama-C 20.0 Calcium, this can be found here. In this document, unsupported constructions appear in red in the relevant BNF rule. Note however that other parts of the manual are left untouched. Notably, the fact that an example is included in the implementation manual does not imply that it is expected to be successfully parsed by the current Frama-C version. In your case, these are the rules of figure 2.17 on page 57, which show that indeed records are not implemented.
As you have already discovered by yourselves, it is indeed possible to define a C struct (possibly ghost) and an ACSL type out of it. Of course, since the struct lives in the C world, its fields must have C types (ACSL types in ghost declarations is unsupported as well).
Similarly, you can simulate the absence of direct record definition by an update (the \with construction) of all the fields of an arbitrary record, as in the following example:
//@ ghost struct c_s { float x; float y; };
//@ type point = struct c_s;
//@ axiomatic Arbitrary_point { logic point empty; }
//@ logic point my_point = {{ empty \with .x = (float)1. } \with .y = (float)2.};