This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Aspect Initial_Condition

This patch provides the initial implementation of aspect/pragma
Initial_Condition. This construct is intended for formal verification proofs.

The construct has the following syntax:

   pragma Initial_Condition (boolean_EXPRESSION);

The construct has the following semantic rules:

The Initial_Condition aspect is introduced by an aspect_specification where the
aspect_mark is Initial_Condition and the aspect_definition shall be a boolean

An Initial_Condition aspect shall only be placed in an aspect_specification of
a package_specification.

Each variable or state abstraction denoted in an Initial_Condition aspect of a
package Q which is declared immediately within the visible part of Q shall be
initialized during the elaboration of Q and be denoted by a name of an
initialization_item of the Initializes aspect of Q.

An Initial_Condition aspect is a sort of postcondition for the elaboration of
both the specification and body of a package. If present on a package, then its
Boolean_expression defines properties (a predicate) of the state of the package
which can be assumed to be true immediately following the elaboration of the
package. [The expression of the Initial_Condition cannot denote a state
abstraction. This means that to express properties of hidden state, functions
declared in the visible part acting on the state abstractions of the package
must be used.]

With respect to dynamic semantics, specifying a given expression as the
Initial_Condition aspect of a package is equivalent to specifying that
expression as the argument of an Assert pragma occurring at the end of the
(possibly implicit) statement list of the (possibly implicit) body of the
package. [This equivalence includes all interactions with pragma
Assertion_Policy. This equivalence does not extend to matters of static
semantics, such as name resolution.] An Initial_Condition expression does not
cause freezing until the point where it is evaluated [, at which point
everything that it might freeze has already been frozen].

-- Source --


package Semantics
   with Abstract_State    =>  State,
        Initializes       => (State, Var_1, Var_2),
        Initial_Condition => (Var_1 = 1 and then Var_2 = 0)
   Var_1 : Integer;
   Var_2 : Integer;

   package Error_1
     with Initial_Condition => (Var_3 > 0)  --  no Initializes
      Var_3 : Integer;
   end Error_1;

   package Error_2
     with Initializes       => (Var_4, Var_5),
          Initial_Condition => (Var_4 = 0)  --  Var_5 missing
      Var_4 : Integer;
      Var_5 : Integer;
   end Error_2;

end Semantics;


package Exec_Body_OK2
  with Initializes       => Var,
       Initial_Condition => (Var = 123)
   Var : Integer := 0;
   procedure Dummy;
end Exec_Body_OK2;

--  exec_body_ok2.adb

package body Exec_Body_OK2 is
   procedure Dummy is begin null; end Dummy;
   Var := 123;
end Exec_Body_OK2;

--  runtime_ok.adb

with Exec_Body_OK2;

procedure Runtime_OK is begin null; end Runtime_OK;


package Exec_Spec_Error
  with Initializes       => Var,
       Initial_Condition => (Var = 123)
   Var : Integer := 0;  --  not 123
end Exec_Spec_Error;

--  runtime_error2.adb

with Exec_Spec_Error;

procedure Runtime_Error2 is begin null; end Runtime_Error2;

-- Compilation and output --

$ gcc -c -gnatd.V
$ gnatmake -q -gnata -gnatd.V runtime_ok.adb
$ gnatmake -q -gnata -gnatd.V runtime_error2.adb
$ ./runtime_ok
$ ./runtime_error2.adb "Initial_Condition" requires the presence of aspect or
  pragma "Initializes" expression of "Initial_Condition" must mention the
  following variables   "Var_5" declared at line 20
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Initial_Condition failed at

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

2013-10-14  Hristian Kirtchev  <>

	* aspects.adb: Add an entry in table Canonical_Aspect for
	* Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Initial_Condition.
	* einfo.adb (Get_Pragma): Include pragma Initial_Condition to
	categorization pragmas.
	* (Get_Pragma): Update comment on usage.
	* exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to
	verify the assertion introduced by pragma Initial_Condition.
	(Expand_N_Package_Declaration): Add a runtime check to
	verify the assertion introduced by pragma Initial_Condition.
	(Expand_Pragma_Initial_Condition): New routine.
	* par-prag: Include pragma Initial_Condition to the list of
	pragmas that do not require special processing by the parser.
	* sem_ch3.adb (Analyze_Declarations): Analyze pragma
	Initial_Condition at the end of the visible declarations.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Initial_Condition.
	Aspect Initial_Condition does not need inspection at freezing.
	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part):
	New routine.
	(Analyze_Pragma): Update all calls
	to Check_Declaration_Order. Add processing for pragma
	Initial_Condition. Initial_Condition is now a valid assertion
	kind.  Add an entry in table Sig_Flags for Initial_Condition.
	(Check_Declaration_Order): Reimplemented to handle arbitrary
	(Is_Valid_Assertion_Kind): Add an entry for
	* (Analyze_Initial_Condition_In_Decl_Part):
	New routine.
	* sem_util.adb (Add_Contract_Item): Pragma Initial_Condition
	can now be associated with a package spec.
	* (Add_Contract_Item): Update comment on usage.
	* Update the documentation of node N_Contract
	* Add new predefined name Initial_Condition. Add
	new pragma id for Initial_Condition.

Attachment: difs
Description: Text document

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]