Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support No_Secondary_Stack restriction #911

Closed
senier opened this issue Jan 19, 2022 · 1 comment · Fixed by #918
Closed

Support No_Secondary_Stack restriction #911

senier opened this issue Jan 19, 2022 · 1 comment · Fixed by #918
Assignees
Labels
generator Related to generator package (SPARK code generation)

Comments

@senier
Copy link
Member

senier commented Jan 19, 2022

The No_Secondary_Stack restriction is not fulfilled by the generated code at the moment:

package Test is
   type M is
      message
         F : Opaque;
      end message;
end Test;
Compile
   [Ada]          rflx-test-m.adb
rflx-test-m.adb:55:18: error: violation of restriction "NO_SECONDARY_STACK" at /home/senier/tmp/RecordFlux/no_secondary_stack/pragmas.adc:1
rflx-test-m.adb:192:07: error: violation of restriction "NO_SECONDARY_STACK" at /home/senier/tmp/RecordFlux/no_secondary_stack/pragmas.adc:1
rflx-test-m.ads:545:18: error: violation of restriction "NO_SECONDARY_STACK" at /home/senier/tmp/RecordFlux/no_secondary_stack/pragmas.adc:1
gprbuild: *** compilation phase failed
make: *** [Makefile:2: build/obj/libtest.a] Error 4

The problem is the Read function that return the unconstrained Bytes type:

   function Read (Ctx : Context) return RFLX_Types.Bytes is
     (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));

We should replace those with procedures and and add pragma Restrictions (No_Secondary_Stack); to our compile tests.

@senier senier created this issue from a note in RecordFlux 0.6 (To do) Jan 19, 2022
@senier senier added generator Related to generator package (SPARK code generation) limitation labels Jan 19, 2022
@senier senier moved this from To do to Implementation in RecordFlux 0.6 Jan 19, 2022
@senier senier assigned senier and treiher and unassigned senier Jan 19, 2022
treiher added a commit that referenced this issue Jan 26, 2022
@treiher
Copy link
Collaborator

treiher commented Jan 26, 2022

GNAT Community 2019 complains about violations of the No_Secondary_Stack restriction, even for functions with Ghost aspect. I don't see a simple workaround, so I would propose to drop support for this version.

While all other compilers ignore the with aunit; in the project file, if AUnit is not used, the FSF GNAT builds the AUnit sources anyway. That leads to a failing compilation if the restriction "No_Secondary_Stack" is enabled. Does anyone see a better workaround than disabling building the AUnit test suite with restrictions for FSF GNAT?

treiher added a commit that referenced this issue Jan 26, 2022
The explicit `clean` is added for GNAT Community 2020 and Pro 20.2. The
compilation of the test suite with restrictions is disabled for FSF
GNAT, as this compiler compiles the AUnit source code, which is
incompatible to the restrictions, regardless of whether it is needed.

Ref. #911
treiher added a commit that referenced this issue Jan 26, 2022
treiher added a commit that referenced this issue Jan 26, 2022
treiher added a commit that referenced this issue Jan 26, 2022
Enabling `-gnata` and `-O` at the same time leads to very long build
times.

Ref. #911
@treiher treiher moved this from Implementation to Review in RecordFlux 0.6 Jan 26, 2022
RecordFlux 0.6 automation moved this from Review to Done Jan 27, 2022
treiher added a commit that referenced this issue Jan 27, 2022
treiher added a commit that referenced this issue Jan 27, 2022
The explicit `clean` is added for GNAT Community 2020 and Pro 20.2. The
compilation of the test suite with restrictions is disabled for FSF
GNAT, as this compiler compiles the AUnit source code, which is
incompatible to the restrictions, regardless of whether it is needed.

Ref. #911
treiher added a commit that referenced this issue Jan 27, 2022
treiher added a commit that referenced this issue Jan 27, 2022
Enabling `-gnata` and `-O` at the same time leads to very long build
times.

Ref. #911
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
generator Related to generator package (SPARK code generation)
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

2 participants