Skip to content

Iss 131 front end #340

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 5 commits into from
Closed

Iss 131 front end #340

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
3451c89
Add Gnatprove_Mode to test suppressing size too small message.
May 7, 2020
92d6e23
Commented out faulty size representation check.
tjj2017 May 7, 2020
1ab19ff
Update test results. Improved error messages.
tjj2017 May 8, 2020
7b6f7e9
Re-instated checks for component size to minimise diffs in itegration…
tjj2017 May 8, 2020
228d91f
Updated golden results reflecting the changes due to commenting out
tjj2017 May 8, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
186 changes: 93 additions & 93 deletions experiments/golden-results/StratoX-summary.txt
View file
Open in desktop

Large diffs are not rendered by default.

5 changes: 0 additions & 5 deletions experiments/golden-results/libkeccak-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,6 @@ Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Precondition
Nkind: N_Pragma
--
Occurs: 190 times
Calling function: Process_Declaration
Error message: size clause not applied by the front-end
Nkind: N_Attribute_Definition_Clause
--
Occurs: 47 times
Calling function: Process_Declaration
Error message: Use type clause declaration
Expand Down
5 changes: 0 additions & 5 deletions experiments/golden-results/libsparkcrypto-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,11 +48,6 @@ Calling function: Do_Itype_Integer_Subtype
Error message: Non-literal bound unsupported
Nkind: N_Defining_Identifier
--
Occurs: 24 times
Calling function: Process_Declaration
Error message: size clause not applied by the front-end
Nkind: N_Attribute_Definition_Clause
--
Occurs: 23 times
Calling function: Do_Expression
Error message: Quantified
Expand Down
110 changes: 55 additions & 55 deletions experiments/golden-results/muen-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,6 @@ Calling function: Process_Declaration
Error message: Use type clause declaration
Nkind: N_Use_Type_Clause
--
Occurs: 56 times
Calling function: Process_Declaration
Error message: size clause not applied by the front-end
Nkind: N_Attribute_Definition_Clause
--
Occurs: 13 times
Calling function: Do_Derived_Type_Definition
Error message: record extension unsupported
Expand Down Expand Up @@ -138,7 +133,7 @@ Redacted compiler error message:
"REDACTED" not declared in "REDACTED"
Raw compiler error message:
--
Occurs: 51 times
Occurs: 49 times
Redacted compiler error message:
violation of restriction "REDACTED"
Raw compiler error message:
Expand Down Expand Up @@ -248,11 +243,6 @@ Redacted compiler error message:
file "REDACTED" not found
Raw compiler error message:
--
Occurs: 5 times
Redacted compiler error message:
violation of restriction "REDACTED"
Raw compiler error message:
--
Occurs: 4 times
Redacted compiler error message:
"REDACTED" depends on "REDACTED"
Expand Down Expand Up @@ -373,6 +363,11 @@ Redacted compiler error message:
missing case values: 3 .. 16#7FFF_FFFF_FFFF_FFFF#
Raw compiler error message:
--
Occurs: 3 times
Redacted compiler error message:
violation of restriction "REDACTED"
Raw compiler error message:
--
Occurs: 2 times
Redacted compiler error message:
"REDACTED" depends on "REDACTED"
Expand Down Expand Up @@ -2735,6 +2730,11 @@ Raw compiler error message:
--
Occurs: 1 times
Redacted compiler error message:
file "REDACTED" not found
Raw compiler error message:
--
Occurs: 1 times
Redacted compiler error message:
incorrect spec in file "REDACTED" must be removed first
Raw compiler error message:
--
Expand Down Expand Up @@ -2980,222 +2980,222 @@ Error detected at REDACTED
--
Occurs: 2 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
Error detected at REDACTED
--
Occurs: 2 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
Expand Down
9 changes: 2 additions & 7 deletions experiments/golden-results/vct-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,6 @@ Calling function: Process_Pragma_Declaration
Error message: Unsupported pragma: Suppress initialization
Nkind: N_Pragma
--
Occurs: 4 times
Calling function: Process_Declaration
Error message: size clause not applied by the front-end
Nkind: N_Attribute_Definition_Clause
--
Occurs: 3 times
Calling function: Do_Expression
Error message: ATTRIBUTE_IMAGE unsupported
Expand Down Expand Up @@ -115,12 +110,12 @@ Raw compiler error message:
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
+===========================GNAT BUG DETECTED==============================+
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
Error detected at REDACTED
--
Occurs: 1 times
Expand Down
Loading