Merge pull request #235 from hannes-steffenhagen-diffblue/feature-cbmc_bump

Feature cbmc bump

Author: hannes-steffenhagen-diffblue

experiments/golden-results/StratoX-summary.txt

@@ -28,7 +28,7 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Global
 Nkind: N_Pragma
 --
-Occurs: 432 times
+Occurs: 430 times
 Calling function: Process_Declaration
 Error message: Package declaration
 Nkind: N_Package_Declaration
@@ -38,27 +38,27 @@ Calling function: Do_Record_Component
 Error message: Wrong component nkind
 Nkind: N_Pragma
 --
-Occurs: 405 times
+Occurs: 403 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Function_Instantiation
 --
-Occurs: 400 times
-Calling function: Do_Function_Call
-Error message: func name not in symbol table
-Nkind: N_Function_Call
---
 Occurs: 398 times
 Calling function: Do_Expression
 Error message: Unknown expression kind
 Nkind: N_Expanded_Name
 --
+Occurs: 397 times
+Calling function: Do_Function_Call
+Error message: func name not in symbol table
+Nkind: N_Function_Call
+--
 Occurs: 348 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Suppress initialization
 Nkind: N_Pragma
 --
-Occurs: 342 times
+Occurs: 340 times
 Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Validate_Unchecked_Conversion
@@ -68,7 +68,7 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Volatile
 Nkind: N_Pragma
 --
-Occurs: 284 times
+Occurs: 283 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Unreferenced
 Nkind: N_Pragma
@@ -103,7 +103,7 @@ Calling function: Do_Type_Definition
 Error message: Unknown expression kind
 Nkind: N_Access_Procedure_Definition
 --
-Occurs: 142 times
+Occurs: 133 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Check
 Nkind: N_Pragma
@@ -118,12 +118,12 @@ Calling function: Do_Expression
 Error message: Unknown attribute
 Nkind: N_Attribute_Reference
 --
-Occurs: 98 times
+Occurs: 90 times
 Calling function: Do_Aggregate_Literal_Array
 Error message: More than one named operand
 Nkind: N_Aggregate
 --
-Occurs: 96 times
+Occurs: 86 times
 Calling function: Do_Expression
 Error message: In
 Nkind: N_In

experiments/golden-results/Tokeneer-summary.txt

@@ -138,11 +138,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Atomic
 Nkind: N_Pragma
 --
-Occurs: 4 times
-Calling function: Do_Aggregate_Literal_Array
-Error message: More than one named operand
-Nkind: N_Aggregate
---
 Occurs: 3 times
 Calling function: Do_Itype_Integer_Subtype
 Error message: Non-literal bound unsupported

experiments/golden-results/UKNI-Information-Barrier-summary.txt

@@ -24,11 +24,6 @@ Error message: Unsupported pragma: Implementation defined
 Nkind: N_Pragma
 --
 Occurs: 1 times
-Calling function: Do_Aggregate_Literal_Array
-Error message: More than one named operand
-Nkind: N_Aggregate
---
-Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Use package clause declaration
 Nkind: N_Use_Package_Clause

experiments/golden-results/libkeccak-summary.txt

@@ -8,46 +8,41 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
 --
-Occurs: 448 times
+Occurs: 442 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Global
 Nkind: N_Pragma
 --
-Occurs: 259 times
+Occurs: 181 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
 Nkind: N_Function_Call
 --
-Occurs: 199 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
-Occurs: 157 times
-Calling function: Do_Function_Call
-Error message: function entity not defining identifier
-Nkind: N_Function_Call
---
 Occurs: 123 times
 Calling function: Do_Procedure_Call_Statement
 Error message: sym id not in symbol table
 Nkind: N_Procedure_Call_Statement
 --
-Occurs: 72 times
+Occurs: 103 times
+Calling function: Do_Constant
+Error message: Constant Type not in symbol table
+Nkind: N_Integer_Literal
+--
+Occurs: 64 times
+Calling function: Process_Declaration
+Error message: Use type clause declaration
+Nkind: N_Use_Type_Clause
+--
+Occurs: 62 times
 Calling function: Make_Array_First_Expr
 Error message: Base type not array type
 Nkind: N_Defining_Identifier
 --
-Occurs: 72 times
+Occurs: 62 times
 Calling function: Make_Array_Index_Op
 Error message: Base type not array type
 Nkind: N_Defining_Identifier
 --
-Occurs: 67 times
-Calling function: Process_Declaration
-Error message: Use type clause declaration
-Nkind: N_Use_Type_Clause
---
 Occurs: 58 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Postcondition
@@ -68,7 +63,7 @@ Calling function: Process_Statement
 Error message: Unknown expression kind
 Nkind: N_Freeze_Entity
 --
-Occurs: 33 times
+Occurs: 25 times
 Calling function: Do_Pragma
 Error message: Unknown pragma name
 Nkind: N_Pragma
@@ -78,17 +73,17 @@ Calling function: Do_Type_Definition
 Error message: Access type unsupported
 Nkind: N_Access_To_Object_Definition
 --
-Occurs: 23 times
-Calling function: Do_Itype_Integer_Subtype
-Error message: Non-literal bound unsupported
-Nkind: N_Defining_Identifier
---
 Occurs: 18 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Suppress initialization
 Nkind: N_Pragma
 --
 Occurs: 16 times
+Calling function: Do_Itype_Integer_Subtype
+Error message: Non-literal bound unsupported
+Nkind: N_Defining_Identifier
+--
+Occurs: 16 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Preelaborable Initialization
 Nkind: N_Pragma
@@ -98,32 +93,22 @@ Calling function: Do_Private_Type_Declaration
 Error message: Abstract type declaration unsupported
 Nkind: N_Private_Type_Declaration
 --
-Occurs: 10 times
-Calling function: Do_Aggregate_Literal_Array
-Error message: More than one named operand
-Nkind: N_Aggregate
---
-Occurs: 10 times
-Calling function: Do_Op_Expon
-Error message: Exponentiation unhandled for non mod types at the moment
-Nkind: N_Op_Expon
---
 Occurs: 9 times
 Calling function: Do_Expression
 Error message: Unknown expression kind
 Nkind: N_Null
 --
-Occurs: 8 times
-Calling function: Do_While_Statement
-Error message: Wrong Nkind spec
-Nkind: N_Loop_Statement
+Occurs: 9 times
+Calling function: Do_Op_Expon
+Error message: Exponentiation unhandled for non mod types at the moment
+Nkind: N_Op_Expon
 --
 Occurs: 8 times
 Calling function: Process_Declaration
 Error message: Abstract subprogram declaration
 Nkind: N_Abstract_Subprogram_Declaration
 --
-Occurs: 8 times
+Occurs: 7 times
 Calling function: Process_Pragma_Declaration
 Error message: Unknown pragma
 Nkind: N_Pragma
@@ -149,11 +134,6 @@ Error message: Package declaration
 Nkind: N_Package_Declaration
 --
 Occurs: 3 times
-Calling function: Do_Itype_Definition
-Error message: Unknown Ekind
-Nkind: N_Defining_Identifier
---
-Occurs: 3 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Procedure_Instantiation
@@ -174,12 +154,22 @@ Error message: Unknown expression kind
 Nkind: N_Expanded_Name
 --
 Occurs: 2 times
+Calling function: Do_While_Statement
+Error message: Wrong Nkind spec
+Nkind: N_Loop_Statement
+--
+Occurs: 2 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Warnings
 Nkind: N_Pragma
 --
 Occurs: 1 times
 Calling function: Do_Aggregate_Literal_Array
+Error message: More than one named operand
+Nkind: N_Aggregate
+--
+Occurs: 1 times
+Calling function: Do_Aggregate_Literal_Array
 Error message: Wrong kind of other choice
 Nkind: N_Aggregate
 --
@@ -194,6 +184,11 @@ Error message: In
 Nkind: N_In
 --
 Occurs: 1 times
+Calling function: Do_Itype_Definition
+Error message: Unknown Ekind
+Nkind: N_Defining_Identifier
+--
+Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Generic declaration
 Nkind: N_Generic_Subprogram_Declaration

experiments/golden-results/muen-summary.txt

@@ -184,11 +184,6 @@ Error message: Unknown expression kind
 Nkind: N_Object_Declaration
 --
 Occurs: 3 times
-Calling function: Do_Aggregate_Literal_Array
-Error message: More than one named operand
-Nkind: N_Aggregate
---
-Occurs: 3 times
 Calling function: Do_Procedure_Call_Statement
 Error message: sym id not in symbol table
 Nkind: N_Procedure_Call_Statement
@@ -209,6 +204,11 @@ Error message: Unhandled aggregate kind
 Nkind: N_Aggregate
 --
 Occurs: 2 times
+Calling function: Do_Aggregate_Literal_Array
+Error message: More than one named operand
+Nkind: N_Aggregate
+--
+Occurs: 2 times
 Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Validate_Unchecked_Conversion

experiments/golden-results/vct-summary.txt

@@ -23,11 +23,6 @@ Calling function: Do_Expression
 Error message: Unknown expression kind
 Nkind: N_Expanded_Name
 --
-Occurs: 11 times
-Calling function: Do_Aggregate_Literal_Array
-Error message: More than one named operand
-Nkind: N_Aggregate
---
 Occurs: 9 times
 Calling function: Do_Private_Type_Declaration
 Error message: Abstract type declaration unsupported
@@ -125,5 +120,10 @@ Raw compiler error message:
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
+| GNU Ada (ada2goto) Assert_Failure failed precondition from goto_utils.ads:115|
+| Error detected at system.ads:156:5                                       |
+--
+Occurs: 1 times
++===========================GNAT BUG DETECTED==============================+
 | GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
 | Error detected at system.ads:156:5                                       |

gnat2goto/driver/arrays.adb

@@ -58,7 +58,9 @@ package body Arrays is
          Low_Expr : constant Irep := Do_Expression (Low_Bound (Bounds));
          High_Expr : constant Irep := Do_Expression (High_Bound (Bounds));
          Index_Type_Node : constant Entity_Id := Etype (Etype (Bounds));
-         Index_Type : constant Irep := Do_Type_Reference (Index_Type_Node);
+         Index_Type : constant Irep := Follow_Symbol_Type
+           (Do_Type_Reference (Index_Type_Node),
+            Global_Symbol_Table);
          Len_Expr : constant Irep :=
            Build_Array_Size (First      => Low_Expr,
                              Last       => High_Expr,
@@ -166,12 +168,10 @@ package body Arrays is
             begin
                if With_Mode then
                   declare
-                     Pos_Str : constant String := Integer'Image (Pos_Number);
-                     Pos_Constant : constant Irep :=
-                       Make_Constant_Expr (Value =>
-                                             Pos_Str (2 .. Pos_Str'Last),
-                                           I_Type => Make_Integer_Type,
-                                           Source_Location => Sloc (N));
+                     Pos_Constant : constant Irep := Integer_Constant_To_Expr
+                       (Value => UI_From_Int (Int (Pos_Number)),
+                        Expr_Type => Index_Type,
+                        Source_Location => No_Location);
                      New_With : constant Irep :=
                        Make_With_Expr (Old => Array_Expr,
                                        Where => Pos_Constant,