Tool fix: use array instead of Ada.Containers.Formal_Hashed_Maps for Com_Map

Ada GPL 2012 does not support Ada.Containers.Formal_Hashed_Maps for
proofs. Use array instead.

Fix proposed by Yannick Moy (AdaCore).

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add specification for Step_Function

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add body of Step_Function.Get_Value. Add test procedure

* Update project switches to compile assertions as dynamic tests.

* Allow Step_Function range in Natural.

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Update loop invariant to prove Step_Function.Get_Value body

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Test Step_Function.Has_Same_Delimiters

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Remove unneeded loop invariant in Step_Function.Get_Value

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Code cleanup: rename Step_Function.Is_Valid_Step_Function into Is_Valid

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add specification for Step_Function.Restrictive_Merge

* Add new Min function specification and body

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Use 8 processes instead of 6 for proofs

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
In Step_Function_Test, check that SFun2 is valid step function

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Refactoring: remove Step_Function.Defaut_Value

* Use Step(0) entry as first value.

* Update tests accordingly.

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Bug fix: fix Step_Function.Restrictive_Merge contract

* Index i and j were mixed.

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Bug fix: Fix contract for Is_Valid, check from first delimiter

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
First attempt at Step_Function.Restrictive_Merge body

* Add auxiliary function Index_Increment with its body and proof.

* All invariants and post-conditions of Restrictive_Merge are not
  proved.

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Simplify step_function_test.adb by removing most prefixes

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Configure GNAT project to produce more debug information

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add test for Restrictive_Merge. Update loop invariants to pass tests

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Simplify loop structure in Restrictive_Merge

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add further loop invariants to prove overflows

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add report skeleton

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>