diff mbox series

[Ada] Disable contract cases on formal containers

Message ID 20211005082634.GA2693555@adacore.com
State New
Headers show
Series [Ada] Disable contract cases on formal containers | expand

Commit Message

Pierre-Marie de Rodat Oct. 5, 2021, 8:26 a.m. UTC 
Just like postconditions, contract cases on formal containers use
functional containers which might leak memory. Disable them.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/a-cfdlli.ads: Use pragma Assertion_Policy to disable
	contract cases at execution.
	* libgnat/a-cfinve.ads: Idem.
	* libgnat/a-cofove.ads: Idem.
	* libgnat/a-cfhase.ads: Idem.
	* libgnat/a-cfhama.ads: Idem.
	* libgnat/a-cforse.ads: Idem.
	* libgnat/a-cforma.ads: Idem.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -44,6 +44,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type List (Capacity : Count_Type) is private with


diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -69,6 +69,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with


diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -67,6 +67,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with


diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -60,6 +60,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    subtype Extended_Index is Index_Type'Base


diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -68,6 +68,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean with


diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -64,6 +64,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean


diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -50,6 +50,7 @@  is
 
    pragma Assertion_Policy (Pre => Ignore);
    pragma Assertion_Policy (Post => Ignore);
+   pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    subtype Extended_Index is Index_Type'Base