search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Structures, Unions and Arrays in logic #67

Closed jensgerlach closed 4 years ago

jensgerlach commented 4 years ago

I am not sure this is the right place for this issue....

The ACSL language implementation document for Frama-C 20.0 shows the following snippet in Example 2.12

//@ type point = struct { real x; real y; };

When processing it with frama-c -wp acsltype.c I receive the following error message

[kernel] Parsing acsltype.c (with preprocessing)
[kernel:annot-error] acsltype.c:2: Warning: unexpected token '{'
[kernel] User Error: warning annot-error treated as fatal error.
...

Do I have to provide more arguments to Frama-C or is it just not yet implemented (it isn't marked as such in the document)?

The error also occurs when changing the snippet into

//@ type point = struct { int x; int y; };
vprevosto commented 4 years ago

Concrete logic types are indeed still unsupported in Frama-C. Hence, this is more a feature request for Frama-C than an ACSL issue. For more details, there was a stackoverflow question on the same subject a few days ago, see my answer there.

jensgerlach commented 4 years ago

Thanks for the pointer to stack overflow !