Merge pull request #346 from tjj2017/nondet_model

Nondet model

Author: martin-cs

experiments/golden-results/StratoX-summary.txt

@@ -8,6 +8,11 @@ Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Validate_Unchecked_Conversion
 --
+Occurs: 163 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Export: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 152 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Postcondition
@@ -33,11 +38,6 @@ Calling function: Do_Expression
 Error message: Last of string unsupported
 Nkind: N_Attribute_Reference
 --
-Occurs: 13 times
-Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Global
-Nkind: N_Pragma
---
 Occurs: 10 times
 Calling function: Do_Expression
 Error message: ATTRIBUTE_MACHINE unsupported
@@ -103,6 +103,11 @@ Calling function: Do_Itype_Integer_Subtype
 Error message: Non-literal bound unsupported
 Nkind: N_Defining_Identifier
 --
+Occurs: 2 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Import: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 1 times
 Calling function: Do_Base_Range_Constraint
 Error message: unsupported lower range kind
@@ -1820,7 +1825,7 @@ Error detected at REDACTED
 --
 Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:73|
+| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:74|
 Error detected at REDACTED
 --
 Occurs: 1 times
@@ -2205,5 +2210,5 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.a
 --
 Occurs: 1 times
 <========================>
-raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:73
+raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:74
 

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

@@ -18,6 +18,11 @@ Calling function: Do_Expression
 Error message: Last of string unsupported
 Nkind: N_Attribute_Reference
 --
+Occurs: 1 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Export: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 5 times
 Redacted compiler error message:
 "REDACTED" not declared in "REDACTED"

experiments/golden-results/ksum-summary.txt

@@ -1,3 +1,8 @@
+Occurs: 1 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Import: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 41 times
 Redacted compiler error message:
 file "REDACTED" not found

experiments/golden-results/libkeccak-summary.txt

@@ -1,10 +1,5 @@
 Occurs: 423 times
 Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Global
-Nkind: N_Pragma
---
-Occurs: 423 times
-Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
 --
@@ -13,6 +8,11 @@ Calling function: Process_Declaration
 Error message: Use type clause declaration
 Nkind: N_Use_Type_Clause
 --
+Occurs: 9 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Import: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 2 times
 Calling function: Do_Expression
 Error message: ATTRIBUTE_ASM_OUTPUT unsupported

experiments/golden-results/libsparkcrypto-summary.txt

@@ -13,11 +13,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Postcondition
 Nkind: N_Pragma
 --
-Occurs: 105 times
-Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Global
-Nkind: N_Pragma
---
 Occurs: 104 times
 Calling function: Process_Pragma_Declaration
 Error message: Unknown pragma: ghost
@@ -48,6 +43,11 @@ Calling function: Do_Itype_Integer_Subtype
 Error message: Non-literal bound unsupported
 Nkind: N_Defining_Identifier
 --
+Occurs: 26 times
+Calling function: Process_Pragma_Declaration
+Error message: pragma Import: Multi-language analysis unsupported
+Nkind: N_Pragma
+--
 Occurs: 23 times
 Calling function: Do_Expression
 Error message: Quantified

experiments/golden-results/muen-summary.txt

@@ -25,11 +25,6 @@ Nkind: N_Pragma
 --
 Occurs: 8 times
 Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Global
-Nkind: N_Pragma
---
-Occurs: 8 times
-Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
 --