Skip to content

Generated code for FSM has restriction No_Streams but no tagged type #1310

@mgrojo

Description

@mgrojo

While trying to use SPARK.Containers.Formal.Unbounded_Hashed_Maps in CoAP_SPARK, I've received this error:

error: "rflx-coap_server-main_loop-fsm.adb" has restriction No_Streams
error: but the following files violate this restriction:
error:   "spark-containers-formal-unbounded_hashed_maps.adb"
gprbind: invocation of gnatbind failed
gprbuild: unable to bind coap_server.adb

According to the GNAT Reference Manual, this restriction "allows optimization of tagged types", but I haven't found any tagged type in the code generated by RecordFlux.

I've tried commenting out this restriction in the generated code, and everything seems to be working fine.

Why is this restriction included? Is it really needed, or is the leftover of a previous use of tagged types?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions