Skip to content

Iss 131 ready #343

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

Merged
merged 5 commits into from
Jun 3, 2020
Merged

Iss 131 ready #343

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
0ef44a7
Suppress "size to small" error from front end which aborts compilation.
tjj2017 May 19, 2020
d4e77fe
Implement a more thorough attribute_size model.
tjj2017 May 19, 2020
ca79862
Add tests for new attribute_size model.
tjj2017 May 19, 2020
d5f0e1e
Update pre-existing test affected by the new attribute_size model.
tjj2017 May 19, 2020
c4eb8be
Update golden results.
tjj2017 May 19, 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
185 changes: 90 additions & 95 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
93 changes: 44 additions & 49 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 @@ -2970,222 +2965,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:108|
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:108|
| 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 @@ -18,11 +18,6 @@ Calling function: Do_Expression
Error message: ATTRIBUTE_COPY_SIGN unsupported
Nkind: N_Attribute_Reference
--
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 @@ -110,12 +105,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