Spark SVD warnings

When SVD files are a subproject you get a lot of warnings when running gnatprove on the base address.

Address => NVIC_Base

‘writing to “NVIC_Periph” is assumed to have no effects on other non-volatile objects.’

Is there a good way to quieten those. Such as exclude the SVD sub project or ideally just silence that particular warning?

If I use the --no-subprojects flag then I get some .ali incorrectly formatted fatal errors.

Perhaps I should use this for faster contract generation anyway. However, I believe case statements in .gpr files prevent gnat studio from being able to edit automatically (I can always comment and uncomment the case statements as needed though)

https://docs.adacore.com/spark2014-docs/html/ug/en/spark_mode.html#specifying-files-to-analyze

project My_Project is

type Modes is (“Compile”, “Analyze”);
Mode : Modes := External (“MODE”, “Compile”);

case Mode is
when “Compile” =>
for Source_Dirs use (…);
when “Analyze” =>
for Source_Dirs use (“dir1”, “dir2”);
for Source_Files use (“file1.ads”, “file2.ads”, “file1.adb”, “file2.adb”);
end case;

end My_Project;

Okay. This might work if I fix files not being built. I think I have some files currently not withed and broken by a refactor. Though I am yet to find out how to get Gnat Studio to set the --no-subprojects flag for the nice highlighting.

Update: Setting the flag under Switches->Gnatprove in project properties; Updates the gpr with Gnat Studio compatible syntax. The SPARK menu doesn’t seem to pick it up though.