ocarina-analyzer-real.adb 108 KB
Newer Older
1
2
3
4
5
6
7
8
------------------------------------------------------------------------------
--                                                                          --
--                           OCARINA COMPONENTS                             --
--                                                                          --
--                O C A R I N A . A N A L Y Z E R . R E A L                 --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
--       Copyright (C) 2009 Telecom ParisTech, 2010-2015 ESA & ISAE.        --
--                                                                          --
-- Ocarina  is free software; you can redistribute it and/or modify under   --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion. Ocarina is distributed in the hope that it will be useful, but     --
-- WITHOUT ANY WARRANTY; without even the implied warranty of               --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                     --
--                                                                          --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception,   --
-- version 3.1, as published by the Free Software Foundation.               --
--                                                                          --
-- You should have received a copy of the GNU General Public License and    --
-- a copy of the GCC Runtime Library Exception along with this program;     --
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
-- <http://www.gnu.org/licenses/>.                                          --
26
--                                                                          --
jhugues's avatar
jhugues committed
27
28
--                 Ocarina is maintained by the TASTE project               --
--                      (taste-users@lists.tuxfamily.org)                   --
29
30
31
--                                                                          --
------------------------------------------------------------------------------

32
with Ocarina.Namet;
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
with Errors;

with Ocarina.Analyzer.Messages;
with Ocarina.Analyzer.REAL.Finder;
with Ocarina.Builder.REAL;
with Ocarina.Instances.REAL_Checker.Queries;
with Ocarina.ME_REAL.Tokens;
with Ocarina.ME_REAL.REAL_Tree.Nodes;
with Ocarina.ME_REAL.REAL_Tree.Utils;
with Ocarina.ME_REAL.REAL_Tree.Nutils;
with Ocarina.ME_REAL.REAL_Tree.Debug;
with Ocarina.ME_AADL.AADL_Tree.Nodes;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
with Ocarina.REAL_Values;
with Ocarina.REAL_Expander;
with Ocarina.REAL_Expander.Flow_Analysis;

package body Ocarina.Analyzer.REAL is

52
   use Ocarina.Namet;
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
   use Errors;
   use Ocarina.Analyzer.REAL.Finder;
   use Ocarina.Analyzer.Messages;
   use Ocarina.Builder.REAL;
   use Ocarina.ME_REAL;
   use Ocarina.ME_REAL.REAL_Tree.Nodes;
   use Ocarina.ME_REAL.REAL_Tree.Utils;
   use Ocarina.ME_REAL.REAL_Tree.Nutils;
   use Ocarina.ME_REAL.REAL_Tree.Debug;

   package ATN renames Ocarina.ME_AADL.AADL_Tree.Nodes;
   package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;
   package RN renames Ocarina.ME_REAL.REAL_Tree.Nodes;
   package RT renames Ocarina.ME_REAL.Tokens;
   package RNU renames Ocarina.ME_REAL.REAL_Tree.Nutils;

   procedure Compute_Selection_Subprogram_Calls
70
71
     (R       :     Node_Id;
      Success : out Boolean);
72
73
74
   --  Check selection expression correctness

   procedure Compute_Verification_Subprogram_Calls
75
76
     (R       :     Node_Id;
      Success : out Boolean);
77
78
79
   --  Check verification expression correctness

   procedure Compute_Return_Subprogram_Calls
80
81
     (R       :     Node_Id;
      Success : out Boolean);
82
83
   --  Check return expression correctness

84
   procedure Check_Requirements_Existance (E : Node_Id; Success : out Boolean);
85
86
87
88
89
90
91
   --  Check weither the requirements are registered as theorems,
   --  and merge the trees.

   function Analyze_Sub_Theorem (R : Node_Id) return Boolean;
   --  Analyze a subtheorem tree

   procedure Analyze_Verification_Expression
92
93
     (E       :     Node_Id;
      Success : out Boolean);
94
95
96
97
98
   --  Check if the verification expression is well-formed,
   --  and then link all set references in parameters to existing sets.
   --  Check verification expression type consistency.

   procedure Analyze_Check_Subprogram_Call
99
100
     (S       :     Node_Id;
      Success : out Boolean);
101
102
103
104
105
   --  Bind sets reference to their related set
   --  Put each kind of parameter in the corresponding list
   --  Determine subprogram real return type

   procedure Get_Property_Type
106
107
108
     (E       :     Node_Id;
      Success : out Boolean;
      Result  : out Return_Type);
109
110
111
   --  Ask Ocarina for the property real type

   procedure Analyze_Subtheorem_Parameters
112
113
     (E       :     Node_Id;
      Success : out Boolean);
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
   --  Analyze subtheorem parameters

   function Find_Variable (E : Name_Id) return Node_Id;
   --  returns a variable, searched by name from both used_var list
   --  (theorem-scoped) and global_variables list (global scope).

   AADL_Tree     : Node_Id;
   AADL_Instance : Node_Id;

   ----------
   -- Init --
   ----------

   procedure Init is
   begin
129
      AADL_Tree     := No_Node;
130
131
      AADL_Instance := No_Node;
      Ocarina.ME_REAL.REAL_Tree.Nutils.Init;
132
      Ocarina.Analyzer.Register_Analyzer (RT.Language, Analyze_Model'Access);
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
   end Init;

   -----------
   -- Reset --
   -----------

   procedure Reset is
   begin
      AADL_Tree := No_Node;
      Ocarina.ME_REAL.REAL_Tree.Nutils.Reset;
   end Reset;

   -------------------------------
   -- Register_Library_Theorems --
   -------------------------------

149
   procedure Register_Library_Theorems (REAL_Library : Node_Id) is
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
      pragma Assert (Kind (REAL_Library) = K_Root_Node);

      N : Node;
      T : Node_Id;
   begin
      if Is_Empty (Theorems (REAL_Library)) then
         return;
      end if;

      T := First_Node (Theorems (REAL_Library));
      while Present (T) loop
         N.Node := T;
         Set_Related_Entity (N.Node, No_Node);
         RNU.Node_List.Append (Library_Theorems, N);
         T := Next_Node (T);
      end loop;
   end Register_Library_Theorems;

   ------------------------
   -- Build_Theorem_List --
   ------------------------

172
   procedure Build_Theorem_List (AADL_Root : Node_Id) is
173
174
175
176
177
178
      NL : RNU.Node_List.Instance;
      N  : Node;
      A  : Node_Id;
      T  : Node_Id;
      It : Natural := RNU.Node_List.First;
   begin
179
180
181
      --  XXX The list of theorem to be checked should be computed
      --  from the instance tree instead

182
183
184
      if Main_Theorem = No_Name then
         --  We walk through all annex clauses to build the list of
         --  theorems to be checked.
185

186
187
188
         NL := Get_REAL_Annexes_List (AADL_Root);
         while It <= RNU.Node_List.Last (NL) loop
            A := ATN.Corresponding_Annex (NL.Table (It).Node);
189

190
191
192
            T := First_Node (Theorems (A));
            while Present (T) loop
               N.Node := T;
193

194
195
               --  Set link to the container AADL component for each
               --  theorem in the annex
196

197
               Set_Related_Entity
198
199
                 (N.Node,
                  ATN.Container_Component (NL.Table (It).Node));
200

201
               --  Append to the list of theorems to be run
202

203
204
205
206
207
208
               RNU.Node_List.Append (To_Run_Theorem_List, N);

               T := Next_Node (T);
            end loop;

            It := It + 1;
209
210
         end loop;

211
      else
Jerome Hugues's avatar
Jerome Hugues committed
212
         --  Otherwise, iterate over Library theorems and fetch the
213
214
215
         --  corresponding theorem.

         RNU.Node_List.Init (To_Run_Theorem_List); --  Reset list of theorems
Jerome Hugues's avatar
Jerome Hugues committed
216

217
218
         for J in RNU.Node_List.First .. RNU.Node_List.Last (Library_Theorems)
         loop
219
220
221
222
223
224
225
226
227
228
229
230
            A := Library_Theorems.Table (J).Node;

            if Main_Theorem = Name (Identifier (A)) then
               N.Node := A;
               Set_Related_Entity (N.Node, AADL_Root);

               --  Append to the list of theorems to be run

               RNU.Node_List.Append (To_Run_Theorem_List, N);
            end if;
         end loop;
      end if;
231
232
233
234
235
236
   end Build_Theorem_List;

   -------------------
   -- Analyze_Model --
   -------------------

237
   function Analyze_Model (Root : Node_Id) return Boolean is
238
239
240
241
242
243
244
245
      use AIN;
      use ATN;
      use Ocarina.Analyzer.REAL;
      use Ocarina.REAL_Expander;
      use Ocarina.REAL_Expander.Flow_Analysis;

      pragma Assert (AIN.Kind (Root) = AIN.K_Architecture_Instance);

246
247
248
      Node    : Node_Id;
      It      : Natural := RNU.Node_List.First;
      Success : Boolean;
249
   begin
250
251
252
      AADL_Tree :=
        ATN.Parent
          (ATN.Namespace (Corresponding_Declaration (Root_System (Root))));
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269

      AADL_Instance := Root;

      --  Build the theorem list

      Build_Theorem_List (AADL_Tree);

      --  Build flows

      Explore_Flows;
      Store_Flows (Root);

      --  Init queries

      Ocarina.Instances.REAL_Checker.Queries.Init (Root);

      while It <= RNU.Node_List.Last (To_Run_Theorem_List) loop
270
         Node          := To_Run_Theorem_List.Table (It).Node;
271
272
273
274
275
276
277
278
279
280
281
282
283
284
         RNU.REAL_Root := Node;

         --  Expansion step

         Ocarina.REAL_Expander.Expand (Node, Success);
         if not Success then
            Display_Analyzer_Error
              (RN.Related_Entity (Node),
               "could not proceed to theorem expansion");
            return False;
         end if;

         --  Analyze step

285
         Ocarina.Analyzer.REAL.Analyze_Theorem (RNU.REAL_Root, Root, Success);
286
287
288
289
290
291
292
293
294
295
296
297
298
         if not Success then
            Display_Analyzer_Error
              (RN.Related_Entity (Node),
               "theorem analysis failed");
            return False;
         end if;

         It := It + 1;
      end loop;

      --  For non-used library theorems, we still analyze them,
      --  since they can be called directly through the API

Jerome Hugues's avatar
Jerome Hugues committed
299
300
301
      for J in RNU.Node_List.First ..
        RNU.Node_List.Last (Library_Theorems) loop
         Node := Library_Theorems.Table (J).Node;
302

Jerome Hugues's avatar
Jerome Hugues committed
303
         RNU.REAL_Root := Node;
304

Jerome Hugues's avatar
Jerome Hugues committed
305
306
307
308
309
310
         if not Analyze_Sub_Theorem (RNU.REAL_Root) then
            Display_Analyzer_Error
              (Root, "could not proceed to theorem analysis");
            return False;
         end if;
      end loop;
311
312
313
314
315
316
317
318
319

      return True;
   end Analyze_Model;

   ---------------------
   -- Analyze_Theorem --
   ---------------------

   procedure Analyze_Theorem
320
321
     (Theorem   :     Node_Id;
      AADL_Root :     Node_Id;
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
      Success   : out Boolean)
   is
      use AIN;

      pragma Assert (RN.Kind (Theorem) = RN.K_Theorem);
      pragma Assert (AIN.Kind (AADL_Root) = AIN.K_Architecture_Instance);
   begin
      AADL_Instance := AADL_Root;

      Compute_Selection_Subprogram_Calls (Theorem, Success);
      if not Success then
         return;
      end if;

      if Present (Return_Expression (Theorem)) then
         Compute_Return_Subprogram_Calls (Theorem, Success);
      else
         Compute_Verification_Subprogram_Calls (Theorem, Success);
      end if;
      if not Success then
         return;
      end if;

      Check_Requirements_Existance (Theorem, Success);
      if not Success then
         return;
      end if;
   end Analyze_Theorem;

   ----------------------------------
   -- Check_Requirements_Existance --
   ----------------------------------

   procedure Check_Requirements_Existance
356
357
     (E       :     Node_Id;
      Success : out Boolean)
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
   is
      pragma Assert (Kind (E) = K_Theorem);

      use Ocarina.REAL_Expander;

      R      : constant List_Id := Required_Theorems (E);
      N, T   : Node_Id;
      Caller : constant Node_Id := RNU.REAL_Root;
   begin
      if not Is_Empty (R) then
         N := First_Node (R);
      else
         N := No_Node;
      end if;

      while Present (N) loop
         T := Find_Declared_Theorem (Theorem_Name (N));

         if No (T) then
            Display_Analyzer_Error
378
379
380
381
              (No_Node,
               Get_Name_String (Theorem_Name (N)) &
               " is not a declared theorem",
               Loc => Loc (N));
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
            Success := False;
            return;
         else
            RNU.REAL_Root := T;
            if not Analyze_Sub_Theorem (RNU.REAL_Root) then
               Display_Analyzer_Error
                 (RN.Related_Entity (E),
                  "could not proceed to sub-theorem analysis");
               Success := False;
               return;
            end if;
            Set_Related_Theorem (N, RNU.REAL_Root);
         end if;

         N := Next_Node (N);
      end loop;
      RNU.REAL_Root := Caller;

      Success := True;
   end Check_Requirements_Existance;

   -------------------------------------------
   -- Compute_Verification_Subprogram_Calls --
   -------------------------------------------

   procedure Compute_Verification_Subprogram_Calls
408
409
     (R       :     Node_Id;
      Success : out Boolean)
410
411
412
413
   is
      pragma Assert (Kind (R) = K_Theorem);
   begin
      Analyze_Verification_Expression (Check_Expression (R), Success);
414
415
      if Success
        and then Returned_Type (Check_Expression (R)) /= RT_Boolean
416
417
        and then Returned_Type (Check_Expression (R)) /= RT_Unknown
      then
418
419
420
421
422
423
424
425
426
427
428
429
430
431
         Display_Analyzer_Error
           (No_Node,
            "Top-level check expression must be a boolean value",
            Loc => Loc (Check_Expression (R)));
         Success := False;
      end if;

   end Compute_Verification_Subprogram_Calls;

   -------------------------------------
   -- Compute_Return_Subprogram_Calls --
   -------------------------------------

   procedure Compute_Return_Subprogram_Calls
432
433
     (R       :     Node_Id;
      Success : out Boolean)
434
435
436
437
438
439
440
441
442
443
444
445
446
   is
      pragma Assert (Kind (R) = K_Theorem);

      T : Return_Type;
      C : constant Node_Id := Check_Expression (Return_Expression (R));
   begin
      Analyze_Verification_Expression (C, Success);
      T := Returned_Type (C);

      case Range_Function (Return_Expression (R)) is
         when FC_MMax | FC_MMin | FC_MSum | FC_MProduct =>
            case T is
               when RT_Unknown =>
447
                  T             := RT_Float;
448
449
450
451
452
453
454
455
                  Error_Loc (1) := Loc (C);
                  DW ("Unable to determine actualy returned type.");

               when RT_Float | RT_Integer =>
                  null;

               when others =>
                  Display_Analyzer_Error
456
457
                    (No_Node,
                     "aggregate function expected a numeric value",
458
459
460
461
462
463
464
                     Loc => Loc (C));
                  Success := False;
            end case;

         when FC_MAll_Equals =>
            case T is
               when RT_Unknown =>
465
                  T             := RT_Boolean;
466
467
468
469
470
471
472
473
                  Error_Loc (1) := Loc (C);
                  DW ("Unable to determine actualy returned type.");

               when RT_Float | RT_Integer =>
                  T := RT_Boolean;

               when others =>
                  Display_Analyzer_Error
474
475
                    (No_Node,
                     "aggregate function expected a numeric value",
476
477
478
479
480
481
                     Loc => Loc (C));
                  Success := False;
            end case;

         when others =>
            Display_Analyzer_Error
482
483
484
              (No_Node,
               "aggregate function unknown",
               Loc => Loc (C));
485
            Success := False;
486
            T       := RT_Error;
487
488
489
490
491
492
493
494
495
      end case;

      if Success then
         case T is
            when RT_Float =>
               null;

            when RT_Integer =>
               Error_Loc (1) := Loc (Return_Expression (R));
496
497
               DW ("Returned integer value will be cast to a float " &
                  "at runtime");
498
499
500

            when RT_Boolean =>
               Error_Loc (1) := Loc (Return_Expression (R));
501
502
               DW ("Returned boolean value will be cast to a float " &
                  "at runtime");
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517

            when others =>
               Display_Analyzer_Error
                 (No_Node,
                  "Top-level return expression must be a numeric value",
                  Loc => Loc (Return_Expression (R)));
               Success := False;
         end case;
      end if;
   end Compute_Return_Subprogram_Calls;

   -------------------------
   -- Analyze_Sub_Theorem --
   -------------------------

518
   function Analyze_Sub_Theorem (R : Node_Id) return Boolean is
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
      use Ocarina.REAL_Expander;

      pragma Assert (Kind (R) = K_Theorem);

      Success : Boolean := True;
   begin
      --  If the used set is not empty then that theorem has already
      --  been analyzed.

      if not Is_Empty (Used_Set (R)) then
         return True;
      end if;

      --  Proceed to expansion and analysis

      Expand (R, Success);
      if Success then
         Analyze_Theorem (R, AADL_Instance, Success);
      end if;

      return Success;
   end Analyze_Sub_Theorem;

   ----------------------------------------
   -- Compute_Selection_Subprogram_Calls --
   ----------------------------------------

   procedure Compute_Selection_Subprogram_Calls
547
548
     (R       :     Node_Id;
      Success : out Boolean)
549
550
551
552
553
554
555
556
557
558
559
560
561
562
   is
      pragma Assert (Kind (R) = K_Theorem);

      D : Node_Id := First_Node (Declarations (R));
   begin
      Success := True;
      while Present (D) loop
         case Kind (D) is

            when K_Set_Declaration =>
               Is_Dependant := False;

               --  Set local set to the local stack

563
564
565
               Append_Node_To_List
                 (Referenced_Var (Local_Variable (D)),
                  Local_Var (REAL_Root));
566
567
568
569

               --  Performs analysis

               Analyze_Verification_Expression
570
571
                 (Selection_Expression (D),
                  Success);
572
573
               if not Success then
                  Display_Analyzer_Error
574
575
                    (No_Node,
                     "Could not analyze set declaration",
576
577
578
579
580
581
                     Loc => Loc (D));
                  return;
               end if;

               --  remove local variable from the local stack

582
583
584
               Remove_Node_From_List
                 (Referenced_Var (Local_Variable (D)),
                  Local_Var (REAL_Root));
585
586
587
588
589

            when K_Variable_Decl_Expression =>
               --  Analyze variable declaration

               Analyze_Verification_Expression
590
591
                 (Check_Expression (Return_Expr (D)),
                  Success);
592
593
               if not Success then
                  Display_Analyzer_Error
594
595
                    (No_Node,
                     "Could not analyze variable declaration",
596
597
598
599
                     Loc => Loc (D));
                  return;
               end if;

600
601
602
               Set_Var_Type
                 (Referenced_Var (Var_Ref (D)),
                  Returned_Type (Check_Expression (Return_Expr (D))));
603
604
605

            when K_Variable_Decl_Compute =>
               declare
606
607
608
                  T      : constant Name_Id := Theorem_Name (D);
                  R      : constant Node_Id := Find_Declared_Theorem (T);
                  Stored : constant Node_Id := REAL_Root;
609
610
               begin
                  if No (R) then
611
612
613
614
                     W_Line
                       ("Error : Theorem " &
                        Get_Name_String (T) &
                        " not found");
615
616
617
618
619
                     Success := False;
                     return;
                  end if;

                  REAL_Root := R;
620
621
622
623
624
                  if not Analyze_Sub_Theorem (REAL_Root) then
                     W_Line
                       ("analyze of sub-theorem " &
                        Get_Name_String (Name (Identifier (REAL_Root))) &
                        " failed");
625
626
627
                     Success := False;
                     return;
                  end if;
628
                  REAL_Root := Stored;
629
630
631
632
633
634
635
636
637
638

                  Set_Related_Theorem (D, R);
                  Set_Var_Type (Referenced_Var (Var_Ref (D)), RT_Float);
                  if Parameters (D) /= No_List then
                     Analyze_Subtheorem_Parameters (D, Success);
                  end if;
               end;

            when others =>
               Display_Analyzer_Error
639
640
                 (No_Node,
                  "unexpected node kind in selection expression",
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
                  Loc => Loc (D));
               Success := False;
               return;

         end case;

         D := Next_Node (D);
      end loop;
   end Compute_Selection_Subprogram_Calls;

   -----------------------------------
   -- Analyze_Subtheorem_Parameters --
   -----------------------------------

   procedure Analyze_Subtheorem_Parameters
656
657
     (E       :     Node_Id;
      Success : out Boolean)
658
659
660
661
662
663
664
665
   is
      pragma Assert (Kind (E) = K_Variable_Decl_Compute);

      ------------------------
      -- Find_Set_Reference --
      ------------------------

      procedure Find_Set_Reference
666
667
        (N       :     Node_Id;
         S       :     Node_Id;
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
         Success : out Boolean)
      is
         M, D : Node_Id;
      begin
         Success := True;

         case Kind (N) is

            when K_Set_Reference =>
               declare
                  TV : Value_Id;
               begin
                  --  We register the predefined set

                  pragma Unreferenced (TV);
                  TV := Get_Set_Type (N);
                  Set_Domain (S, N);
               end;

            when K_Identifier =>
688
689
               D :=
                 Find_Node_By_Name (To_Lower (Name (N)), Used_Set (REAL_Root));
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
               if Present (D) then

                  --  Add to set reference list

                  M := Make_Set_Reference;
                  Set_Referenced_Set (M, D);
                  Set_Domain (S, M);
               else

                  --  Can be :
                  --  * a reference on "range" variable
                  --  * any element variable
                  --  * a predefined set (including local_set)

                  --  Search related variable in global list

                  D := Find_Variable (To_Lower (Name (N)));
                  if Present (D) then
                     if Var_Type (D) = RT_Element then
                        M := Make_Var_Reference (Name (N));
                        Set_Referenced_Var (M, D);
                        Set_Domain (S, M);
                     else
                        Display_Analyzer_Error
714
715
                          (No_Node,
                           Get_Name_String (Name (N)) &
716
717
718
719
720
721
722
723
                           " variable is not an element of a set",
                           Loc => Loc (N));
                        Success := False;
                        return;
                     end if;

                  elsif Get_Name_String (Name (N)) = "local_set" then
                     declare
724
725
726
                        T   : Value_Id;
                        NM  : Name_Id;
                        Set : Node_Id;
727
728
729
730
731
732
                     begin
                        M := Make_Set_Reference;

                        T := SV_Local_Set;
                        Set_Str_To_Name_Buffer
                          (Ocarina.ME_REAL.Tokens.Image
733
                             (Translate_Predefined_Sets (T)));
734
735
736
737
738
739
740
741
742
743
744
745
746
747
                        NM := Name_Find;

                        --  Create a set in order to register actual use
                        --  of the predefined set

                        Set := Make_Set (NM, T);
                        Set_Predefined_Type (Set, T);
                        Set_Referenced_Set (M, Set);
                        Set_Set_Type (Set, T);
                        Append_Node_To_List (Set, Used_Set (REAL_Root));

                        Set_Domain (S, M);
                     end;
                  else
748
749
750
751
752
753
754
                     Display_Analyzer_Error
                       (No_Node,
                        Get_Name_String (Name (N)) &
                        " is not a declared set or variable",
                        Loc => Loc (N));
                     Success := False;
                     return;
755
756
757
758
                  end if;
               end if;

            when others =>
759
760
761
762
               Display_Analyzer_Error
                 (No_Node,
                  "wrong parameter type",
                  Loc => Loc (N));
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
               Success := False;
         end case;
      end Find_Set_Reference;

      N : Node_Id := First_Node (Parameters (E));
      P : Node_Id;
      D : Node_Id;
   begin
      Success := True;

      if not Present (N) then
         Set_Domain (E, No_Node);
         return;
      end if;

      Find_Set_Reference (N, E, Success);
779
      Set_True_params (E, New_List (K_List_Id, Loc (E)));
780
      if not Success then
781
782
783
784
         Display_Analyzer_Error
           (No_Node,
            "First parameter of subprogram " & "call is not a set",
            Loc => Loc (N));
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
         return;
      end if;

      N := Next_Node (N);
      while Present (N) loop
         case Kind (N) is

            when K_Literal =>
               P := New_Node (K_Literal, Loc (N));
               Set_Value (P, Value (N));
               declare
                  use Ocarina.REAL_Values;
                  V : constant Value_Type := Get_Value_Type (Value (N));
               begin
                  case V.T is
                     when LT_Integer =>
                        Set_Returned_Type (P, RT_Integer);

                     when LT_Real =>
                        Set_Returned_Type (P, RT_Float);

                     when LT_String =>
                        Set_Returned_Type (P, RT_String);

809
                     when LT_Boolean =>
810
811
812
813
814
815
816
                        Set_Returned_Type (P, RT_Boolean);

                     when LT_Enumeration =>
                        Set_Returned_Type (P, RT_String);

                     when others =>  -- Can't happen
                        Display_Analyzer_Error
817
818
819
                          (No_Node,
                           "unexpected value type in literal",
                           Loc => Loc (N));
820
821
822
823
824
825
826
827
828
829
830
831
832
833
                        Success := False;
                        return;
                  end case;
               end;
               Append_Node_To_List (P, True_params (E));

            when K_Identifier =>
               D := Find_Variable (To_Lower (Name (N)));
               if Present (D) then
                  P := Make_Var_Reference (Name (N));
                  Set_Referenced_Var (P, D);
                  Append_Node_To_List (P, True_params (E));
               else
                  Display_Analyzer_Error
834
835
                    (No_Node,
                     "could not find variable " &
836
837
838
839
840
841
842
843
                     Get_Name_String (To_Lower (Name (N))),
                     Loc => Loc (N));
                  Success := False;
                  return;
               end if;

            when others =>
               Display_Analyzer_Error
844
845
846
847
                 (No_Node,
                  "subtheorem parameter " &
                  "must be a literal or an identifier",
                  Loc => Loc (N));
848
849
850
851
852
853
854
855
856
857
858
859
860
               Success := False;
               return;
         end case;

         N := Next_Node (N);
      end loop;
   end Analyze_Subtheorem_Parameters;

   -------------------------------------
   -- Analyze_Verification_Expression --
   -------------------------------------

   procedure Analyze_Verification_Expression
861
862
     (E       :     Node_Id;
      Success : out Boolean)
863
864
865
   is
      use Ocarina.REAL_Values;

866
867
868
869
870
871
      pragma Assert
        (Kind (E) = K_Check_Expression
         or else Kind (E) = K_Ternary_Expression
         or else Kind (E) = K_Literal
         or else Kind (E) = K_Var_Reference
         or else Kind (E) = K_Check_Subprogram_Call);
872

873
874
      T1, T2       : Return_Type;
      V            : Value_Type;
875
876
877
878
      Part_Unknown : Boolean;
   begin
      Success := True;

879
      case Kind (E) is
880
881
882
883
884
885
886
887
888
889
         when K_Var_Reference =>  --  Found a variable
            declare
               N : Node_Id;
            begin
               N := Find_Variable (To_Lower (Name (E)));

               --  The variable must have been previsously
               --  defined andd analyzed.

               if No (N) then
890
891
892
893
                  N :=
                    Find_Node_By_Name
                      (To_Lower (Name (E)),
                       Local_Var (REAL_Root));
894
895
                  if No (N) then
                     Display_Analyzer_Error
896
897
                       (No_Node,
                        "could not find variable " &
898
899
900
901
902
903
904
905
906
                        Get_Name_String (To_Lower (Name (E))),
                        Loc => Loc (E));
                     Success := False;
                     return;
                  end if;
               end if;

               if Var_Type (N) = No_Value then
                  Display_Analyzer_Error
907
908
909
                    (No_Node,
                     Get_Name_String (To_Lower (Name (E))) &
                     " is being used before being defined",
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
                     Loc => Loc (E));
                  Success := False;
                  return;
               end if;
               Set_Referenced_Var (E, N);
               Set_Returned_Type (E, Var_Type (N));
            end;

         when K_Check_Subprogram_Call =>
            Analyze_Check_Subprogram_Call (E, Success);

         when K_Literal =>
            V := Get_Value_Type (Value (E));
            case V.T is
               when LT_Integer =>
                  Set_Returned_Type (E, RT_Integer);

               when LT_Real =>
                  Set_Returned_Type (E, RT_Float);

               when LT_String =>
                  Set_Returned_Type (E, RT_String);

933
               when LT_Boolean =>
934
935
936
937
938
939
940
                  Set_Returned_Type (E, RT_Boolean);

               when LT_Enumeration =>
                  Set_Returned_Type (E, RT_String);

               when others =>
                  Display_Analyzer_Error
941
942
                    (No_Node,
                     "unexpected value type in literal",
943
944
945
946
947
948
949
950
951
952
                     Loc => Loc (E));
                  Success := False;
                  return;
            end case;

         when K_Ternary_Expression =>
            Analyze_Verification_Expression (Left_Expr (E), Success);
            if Success then
               Analyze_Verification_Expression (Right_Expr (E), Success);
            end if;
953

954
955
956
957
958
959
960
            if Success then
               Analyze_Verification_Expression (Third_Expr (E), Success);
            end if;
            if Success then
               T1 := Returned_Type (Left_Expr (E));
               if T1 /= RT_Boolean then
                  Display_Analyzer_Error
961
962
963
                    (No_Node,
                     "Ternary expression must begin by a boolean " &
                     "expression ",
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
                     Loc => Loc (E));
                  Success := False;
                  return;
               end if;
               T1 := Returned_Type (Right_Expr (E));
               T2 := Returned_Type (Third_Expr (E));
               if T1 = T2 then
                  Set_Returned_Type (E, T1);
               else
                  Set_Returned_Type (E, RT_Unknown);
               end if;
            end if;
            if not Success then
               return;
            end if;

         when K_Check_Expression =>
981
            if Present (Left_Expr (E)) and then Present (Right_Expr (E)) then
982
               Analyze_Verification_Expression (Left_Expr (E), Success);
983

984
985
986
               if Success then
                  Analyze_Verification_Expression (Right_Expr (E), Success);
               end if;
987

988
989
990
               if not Success then
                  return;
               end if;
991
992
               T1           := Returned_Type (Left_Expr (E));
               T2           := Returned_Type (Right_Expr (E));
993
994
995
996
997
               Part_Unknown := (T1 = RT_Unknown or else T2 = RT_Unknown);

               case Operator (E) is
                  when OV_And | OV_Or =>
                     if not Part_Unknown then
998
                        if T1 /= RT_Boolean or else T2 /= RT_Boolean then
999
                           Display_Analyzer_Error
1000
1001
1002
1003
                             (No_Node,
                              "Inconsistent types in expression " &
                              "<boolean_operator> : " &
                              "must be boolean sub-expressions",
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
                              Loc => Loc (E));
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Boolean);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Boolean);
                     end if;

                  when OV_Equal =>
                     if not Part_Unknown then
                        if T1 /= T2 then
                           Display_Analyzer_Error
1018
1019
                             (No_Node,
                              "Inconsistent types in expression '='",
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
                              Loc => Loc (E));
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Boolean);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Boolean);
                     end if;

                  when OV_Different =>
                     if not Part_Unknown then
                        if T1 /= T2 then
                           Display_Analyzer_Error
1034
1035
                             (No_Node,
                              "Inconsistent types in expression '<>'",
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
                              Loc => Loc (E));
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Boolean);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Boolean);
                     end if;

1046
1047
1048
1049
                  when OV_Greater    |
                    OV_Less          |
                    OV_Less_Equal    |
                    OV_Greater_Equal =>
1050
                     if not Part_Unknown then
1051
1052
                        if (T2 /= RT_Float and then T2 /= RT_Integer)
                          or else (T1 /= RT_Float and then T1 /= RT_Integer)
1053
                        then
1054
                           Display_Analyzer_Error
1055
1056
1057
1058
                             (No_Node,
                              "Inconsistent types in expression " &
                              "<comparator>",
                              Loc => Loc (E));
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Boolean);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Boolean);
                     end if;

                  when OV_Plus =>
                     if not Part_Unknown
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
                       and then
                       ((T1 /= T2
                         and then
                         ((T1 /= RT_Float and then T1 /= RT_Integer)
                          or else (T2 /= RT_Float and then T2 /= RT_Integer)))
                        or else
                        (T1 = RT_Boolean
                         or else T1 = RT_Element
                         or else T1 = RT_Range
                         or else T1 = RT_String
                         or else T1 = RT_Error))
                     then
1082
                        Display_Analyzer_Error
1083
1084
                          (No_Node,
                           "Inconsistent types in expression +|-",
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
                           Loc => Loc (E));
                        Success := False;
                        return;
                     else
                        if T1 = T2 and then T1 = RT_Integer then
                           Set_Returned_Type (E, RT_Integer);
                        elsif T1 = RT_Float or else T2 = RT_Float then
                           Set_Returned_Type (E, RT_Float);
                        else
                           Set_Returned_Type (E, T1);
                        end if;
                     end if;

                  when OV_Modulo =>
                     if not Part_Unknown
1100
1101
                       and then (T2 /= RT_Integer or else T1 /= RT_Integer)
                     then
1102
                        Display_Analyzer_Error
1103
1104
                          (No_Node,
                           "Inconsistent types for operator ",
1105
1106
1107
1108
1109
1110
1111
1112
1113
                           Loc => Loc (E));
                        Success := False;
                        return;
                     else
                        Set_Returned_Type (E, RT_Integer);
                     end if;

                  when OV_Minus | OV_Star | OV_Slash | OV_Power =>
                     if not Part_Unknown
1114
1115
1116
1117
                       and then
                       ((T2 /= RT_Float and then T2 /= RT_Integer)
                        or else (T1 /= RT_Float and then T1 /= RT_Integer))
                     then
1118
                        Display_Analyzer_Error
1119
1120
                          (No_Node,
                           "Inconsistent types in expression +|-",
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
                           Loc => Loc (E));
                        Success := False;
                        return;
                     else
                        if T1 = T2 and then T1 = RT_Integer then
                           Set_Returned_Type (E, RT_Integer);
                        else
                           Set_Returned_Type (E, RT_Float);
                        end if;
                     end if;

                  when others =>
                     Display_Analyzer_Error
1134
1135
1136
                       (No_Node,
                        "unexpected operator",
                        Loc => Loc (E));
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
                     Success := False;
                     return;
               end case;

            elsif Present (Right_Expr (E)) then
               Analyze_Verification_Expression (Right_Expr (E), Success);
               if not Success then
                  return;
               end if;
               T1 := Returned_Type (Right_Expr (E));

               case Operator (E) is

                  when OV_Not =>
                     if not Part_Unknown then
                        if T1 /= RT_Boolean then
                           Display_Analyzer_Error
1154
1155
1156
                             (No_Node,
                              "Inconsistent type in expression, " &
                              "must be boolean",
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
                              Loc => Loc (E));
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Boolean);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Boolean);
                     end if;

                  when OV_Minus =>
                     if not Part_Unknown then
                        if T1 /= RT_Integer and then T1 /= RT_Float then
                           Display_Analyzer_Error
1171
1172
1173
1174
                             (No_Node,
                              "Inconsistent type in expression, " &
                              "must be numeric",
                              Loc => Loc (E));
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
                           Success := False;
                           return;
                        else
                           Set_Returned_Type (E, RT_Unknown);
                        end if;
                     else
                        Set_Returned_Type (E, RT_Float);
                     end if;

                  when others =>
                     Display_Analyzer_Error
1186
1187
1188
                       (No_Node,
                        "unexpected operator",
                        Loc => Loc (E));
1189
1190
1191
1192
1193
1194
1195
                     Success := False;
                     return;
               end case;
            end if;

         when others =>
            Display_Analyzer_Error
1196
1197
1198
              (No_Node,
               "unexpected node kind",
               Loc => Loc (E));
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
            Success := False;
            return;
      end case;
   end Analyze_Verification_Expression;

   -----------------------------------
   -- Analyze_Check_Subprogram_Call --
   -----------------------------------

   procedure Analyze_Check_Subprogram_Call
1209
1210
     (S       :     Node_Id;
      Success : out Boolean)
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
   is
      pragma Assert (Kind (S) = K_Check_Subprogram_Call);

      N : Node_Id := First_Node (Parameters (S));
      M : Node_Id;
      P : Node_Id;
      D : Node_Id;
      T : Return_Type;

      ------------------------
      -- Find_Set_Reference --
      ------------------------

      procedure Find_Set_Reference
1225
1226
1227
        (N       :     Node_Id;
         S       :     Node_Id;
         Is_Set  : out Boolean;
1228
1229
1230
1231
1232
         Success : out Boolean)
      is
         M : Node_Id;
      begin
         Success := True;
1233
         Is_Set  := True;
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
         case Kind (N) is

            when K_Set_Reference =>
               --  We register the predefined set

               declare
                  TV : Value_Id;
               begin
                  pragma Unreferenced (TV);
                  TV := Get_Set_Type (N);
                  Append_Node_To_List (N, Referenced_Sets (S));
               end;

            when K_Identifier =>
1248
1249
               D :=
                 Find_Node_By_Name (To_Lower (Name (N)), Used_Set (REAL_Root));
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
               if Present (D) then
                  --  Add to set reference list

                  M := Make_Set_Reference;
                  Set_Referenced_Set (M, D);
                  Append_Node_To_List (M, Referenced_Sets (S));
               else
                  --  Must be a reference on "range" variable
                  --  or a variable referencing an element of a
                  --  set.

                  if Get_Name_String
1262
1263
1264
1265
1266
1267
                      (Name
                         (Identifier
                            (Range_Variable
                               (Range_Declaration (REAL_Root))))) =
                    Get_Name_String (To_Lower (Name (N)))
                  then
1268
1269
1270
1271
1272

                     M := Make_Set_Reference;
                     Set_Referenced_Set
                       (M,
                        Referenced_Set
1273
1274
1275
                          (Set_Reference
                             (Range_Variable
                                (Range_Declaration (REAL_Root)))));
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
                     Append_Node_To_List (M, Referenced_Sets (S));
                     Is_Set := False;
                  else
                     --  Search related variable

                     declare
                        Found  : Boolean := False;
                        Ignore : Boolean := False;
                     begin
                        --  1/ In global and theorem lists

                        D := Find_Variable (To_Lower (Name (N)));
1288
                        if Present (D) and then Var_Type (D) = RT_Element then
1289
                           Is_Set := False;
1290
                           M      := Make_Var_Reference (Name (N));
1291
                           Set_Referenced_Var (M, D);
1292
                           Append_Node_To_List (M, True_Parameters (S));
1293
1294
                           Found := True;
                        else
1295
1296
1297
                           if Present (D)
                             and then Var_Type (D) = RT_Unknown
                           then
1298
                              DW (Get_Name_String (Name (N)) &
1299
                                 " variable cannot be typed.");
1300
1301
1302
1303
1304
1305
1306
                              Ignore := True;
                           end if;
                        end if;

                        --  1/ In local list

                        if not Found and then not Ignore then
1307
1308
1309
1310
1311
1312
1313
                           D :=
                             Find_Node_By_Name
                               (To_Lower (Name (N)),
                                Local_Var (REAL_Root));
                           if Present (D)
                             and then Var_Type (D) = RT_Element
                           then
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
                              --  Set the variable position

                              if Variable_Position (S) = Value_Id (0) then
                                 if N = First_Node (Parameters (S)) then
                                    Set_Variable_Position (S, Value_Id (1));
                                 else
                                    Set_Variable_Position (S, Value_Id (2));
                                 end if;
                              else
                                 Display_Analyzer_Error
1324
1325
1326
                                   (No_Node,
                                    Get_Name_String (Name (N)) &
                                    " variable is already referenced",
1327
1328
1329
1330
1331
1332
                                    Loc => Loc (N));
                                 Success := False;
                                 return;
                              end if;

                              Is_Set := False;
1333
                              M      := Make_Var_Reference (Name (N));
1334
                              Set_Referenced_Var (M, D);
1335
                              Append_Node_To_List (M, True_Parameters (S));
1336
1337
                              Found := True;
                           else
1338
1339
1340
                              if Present (D)
                                and then Var_Type (D) = RT_Unknown
                              then
1341
                                 DW (Get_Name_String (Name (N)) &
1342
                                    " variable cannot be typed.");
1343
1344
1345
1346
1347
1348
1349
1350
                                 Ignore := True;
                              end if;
                           end if;
                        end if;

                        if not Found then
                           if not Ignore then
                              Display_Analyzer_Error
1351
1352
1353
1354
                                (No_Node,
                                 Get_Name_String (Name (N)) &
                                 " variable is not a " &
                                 "declared set or variable",
1355
1356
1357
1358
1359
                                 Loc => Loc (N));
                              Success := False;
                              return;
                           else
                              Is_Set := False;
1360
                              M      := Make_Var_Reference (Name (N));
1361
                              Set_Referenced_Var (M, D);
1362
                              Append_Node_To_List (M, True_Parameters (S));
1363
1364
1365
1366
1367
1368
1369
1370
                           end if;
                        end if;
                     end;
                  end if;
               end if;

            when others =>
               Display_Analyzer_Error
1371
1372
                 (No_Node,
                  "unexpected node kind as a parameter",
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
                  Loc => Loc (N));
               Success := False;
               return;
         end case;
      end Find_Set_Reference;

      Var : Node_Id;
   begin
      Success := True;
      Set_Referenced_Sets (S, New_List (K_List_Id, Loc (S)));
      Set_True_Parameters (S, New_List (K_List_Id, Loc (S)));

1385
      --  There are three kinds of verification subprogram :
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405

      --  Set-based subprogram, which always takes a  set or
      --  element as first parameter, and can have others
      --  parameters (usually literal). They always returns
      --  a value or a list of values. eg : Cardinal,
      --  Get_Property_Value, Property_Exists.

      --  Value manipulation subprograms (eg. Max, Sum, First,
      --  Last...), where the single parameter is a value or a
      --  list of values, and which returns another value.

      --  The Expr subprogram (iterative expression) compute an
      --  expression on all the elements of the parameter-passed
      --  set, and returns a list of values.

      case Code (S) is

         when FC_Expr =>
            if Present (N)
              and then Present (Next_Node (N))
1406
1407
              and then Present (Next_Node (Next_Node (N)))
            then
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424

               --  The first parameter must be a set

               case Kind (N) is
                  when K_Set_Reference =>

                     --  We register the predefined set

                     declare
                        TV : Value_Id;
                     begin
                        pragma Unreferenced (TV);
                        TV := Get_Set_Type (N);
                        Append_Node_To_List (N, Referenced_Sets (S));
                     end;

                  when K_Identifier =>
1425
1426
1427
1428
                     D :=
                       Find_Node_By_Name
                         (To_Lower (Name (N)),
                          Used_Set (REAL_Root));
1429
1430
1431
1432
1433
1434
1435
1436
1437
                     if Present (D) then

                        --  Add to set reference list

                        M := Make_Set_Reference;
                        Set_Referenced_Set (M, D);
                        Append_Node_To_List (M, Referenced_Sets (S));
                     else
                        Display_Analyzer_Error
1438
1439
1440
                          (No_Node,
                           Get_Name_String (Name (N)) &
                           " is not a declared set or variable",
1441
1442
1443
1444
1445
1446
1447
                           Loc => Loc (N));
                        Success := False;
                        return;
                     end if;

                  when others =>
                     Display_Analyzer_Error
1448
1449
                       (No_Node,
                        "unexpected node kind as a parameter",
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
                        Loc => Loc (N));
                     Success := False;
                     return;
               end case;

               --  The second parameter must be a new variable

               N := Next_Node (N);
               case Kind (N) is
                  when K_Identifier =>
                     --  Check weither the variable is already used

                     D := Find_Variable (To_Lower (Name (N)));
                     if No (D) then

                        --  Declare the new variable

                        P := Make_Variable (Name (N));
                        Set_Var_Type (P, RT_Element);
1469
                        Append_Node_To_List (P, Used_Var (REAL_Root));
1470
1471
1472
1473
1474
1475
1476
1477

                        --  Bind the new variable to the expression

                        M := Make_Var_Reference (Name (N));
                        Set_Referenced_Var (M, P);
                        Append_Node_To_List (M, True_Parameters (S));
                     else
                        Display_Analyzer_Error
1478
1479
1480
                          (No_Node,
                           Get_Name_String (Name (Identifier (N))) &
                           " is already declared",
1481
1482
1483
1484
1485
1486
1487
                           Loc => Loc (N));
                        Success := False;
                        return;
                     end if;

                  when others =>
                     Display_Analyzer_Error
1488
1489
                       (No_Node,
                        "unexpected node kind as a parameter",
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
                        Loc => Loc (N));
                     Success := False;
                     return;
               end case;

               --  The last parameter must be an expression

               N := Next_Node (N);
               case Kind (N) is

1500
1501
1502
                  when K_Check_Subprogram_Call |
                    K_Check_Expression         |
                    K_Ternary_Expression       =>
1503
1504
                     Analyze_Verification_Expression (N, Success);
                     if Success then
1505
                        case Returned_Type (N) is
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
                           when RT_Float =>
                              Set_Returned_Type (S, RT_Float_List);
                           when RT_Integer =>
                              Set_Returned_Type (S, RT_Int_List);
                           when RT_String =>
                              Set_Returned_Type (S, RT_String_List);
                           when RT_Boolean =>
                              Set_Returned_Type (S, RT_Bool_List);
                           when RT_Range =>
                              Set_Returned_Type (S, RT_Range_List);
                           when others =>
                              Display_Analyzer_Error
1518
1519
                                (No_Node,
                                 "could not resolve expression type",
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
                                 Loc => Loc (N));
                              Success := False;
                              return;
                        end case;
                        Remove_Node_From_List (N, Parameters (S));
                        Append_Node_To_List (N, True_Parameters (S));
                     else
                        return;
                     end if;

                  when others =>
                     Display_Analyzer_Error
1532
1533
                       (No_Node,
                        "unexpected node kind as a parameter",
1534
1535
1536
1537
1538
                        Loc => Loc (N));
                     Success := False;
                     return;
               end case;
            else
1539
1540
1541
1542
               Display_Analyzer_Error
                 (No_Node,
                  "expected 3 parameters",
                  Loc => Loc (S));
1543
1544
1545
1546
1547
               Success := False;
               return;
            end if;

         when FC_Get_Property_Value =>
1548
            if Present (N) and then Present (Next_Node (N)) then
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
               declare
                  Is_Set : Boolean;
               begin
                  --  Search related set

                  if Kind (N) = K_Identifier then
                     Find_Set_Reference (N, S, Is_Set, Success);
                  else
                     Success := False;
                  end if;

                  if not Success then
                     Display_Analyzer_Error
1562
1563
                       (No_Node,
                        "first parameter must be a declared set",
1564
1565
1566
1567
1568
1569
1570
1571
1572
                        Loc => Loc (N));
                     return;
                  end if;

                  N := Next_Node (N);
                  if Kind (N) = K_Literal then
                     Get_Property_Type (N, Success, T);
                     if not Success then
                        Display_Analyzer_Error
1573
1574
                          (No_Node,
                           "could not analyze second parameter type",
1575
1576
1577
1578
1579
1580
1581
                           Loc => Loc (N));
                        return;
                     end if;
                     Set_Returned_Type (S, T);

                     P := New_Node (K_Literal, Loc (N));
                     Set_Value (P, Value (N));
1582
                     Append_Node_To_List (P, True_Parameters (S));
1583
1584
                  else
                     Display_Analyzer_Error
1585
1586
                       (No_Node,
                        "second parameter must be a literal",
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
                        Loc => Loc (N));
                     Success := False;
                     return;
                  end if;

                  if Is_Set then
                     case Value_Id (T) is
                        when RT_Float =>
                           Set_Returned_Type (S, RT_Float_List);
                        when RT_Integer =>
                           Set_Returned_Type (S, RT_Int_List);
                        when RT_String =>
                           Set_Returned_Type (S, RT_String_List);
                        when RT_Boolean =>
                           Set_Returned_Type (S, RT_Bool_List);
                        when RT_Range =>
                           Set_Returned_Type (S, RT_Range_List);
                        when RT_String_List =>
                           Set_Returned_Type (S, RT_String_List);
                        when RT_Float_List =>
                           Set_Returned_Type (S, RT_Float_List);
                        when RT_Int_List =>
                           Set_Returned_Type (S, RT_Int_List);
                        when RT_Bool_List =>
                           Set_Returned_Type (S, RT_Bool_List);
                        when RT_Range_List =>
                           Set_Returned_Type (S, RT_Range_List);
1614
1615
                        when RT_Element_List =>
                           Set_Returned_Type (S, RT_Element_List);
1616
1617
                        when others =>
                           Display_Analyzer_Error
1618
1619
1620
                             (No_Node,
                              "Could not resolve list type " &
                              Value_Id (T)'Img,
1621
1622
1623
1624
1625
1626
1627
1628
1629
                              Loc => Loc (N));
                           Success := False;
                           return;
                     end case;
                  else
                     Set_Returned_Type (S, Value_Id (T));
                  end if;
               end;
            else
1630
1631
1632
1633
               Display_Analyzer_Error
                 (No_Node,
                  "expected a parameter",
                  Loc => Loc (S));
1634
1635
1636
1637
1638
               Success := False;
               return;
            end if;

         when FC_Property_Exists =>
1639
            if Present (N) and then Present (Next_Node (N)) then
1640
1641
1642
1643
1644
1645
1646
               declare
                  Is_Set : Boolean;
               begin

                  Find_Set_Reference (N, S, Is_Set, Success);
                  if not Success then
                     Display_Analyzer_Error
1647
1648
1649
1650
                       (No_Node,
                        "Could not find back set related to " &
                        Get_Name_String (Name (N)),
                        Loc => Loc (N));
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
                     Success := False;
                     return;
                  end if;

                  N := Next_Node (N);
                  case Kind (N) is

                     when K_Literal =>
                        P := New_Node (K_Literal, Loc (N));
                        Set_Value (P, Value (N));
1661
                        Append_Node_To_List (P, True_Parameters (S));
1662
1663
1664

                     when others =>
                        Display_Analyzer_Error
1665
1666
                          (No_Node,
                           "unexpected node kind as a parameter",
1667
1668
1669
1670
1671
1672
1673
1674
                           Loc => Loc (N));
                        Success := False;
                        return;
                  end case;
                  Set_Returned_Type (S, RT_Boolean);
               end;
            else
               Display_Analyzer_Error
1675
1676
1677
                 (No_Node,
                  "expected a parameter",
                  Loc => Loc (N));
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
               Success := False;
               return;
            end if;

         when FC_First | FC_Last =>
            if Present (N) then
               case Kind (N) is
                  when K_Check_Subprogram_Call =>
                     Analyze_Check_Subprogram_Call (N, Success);
                     if not Success then
                        return;
                     end if;

1691
                     case Returned_Type (N) is
1692
1693
1694
1695
1696
1697
1698