Skip to content

Nondet model #346

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 6 commits into from
Jun 4, 2020
Merged

Nondet model #346

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9e4a64c
Add basic ASVAT interface modelling support.
tjj2017 May 26, 2020
ebcd004
The output of two testsuite programs has changed.
tjj2017 May 26, 2020
c1bdd71
Add tests for ASVAT modelling features.
tjj2017 May 26, 2020
4fbe906
Remove support for specifying ASVAT models via a pragma Import.
tjj2017 May 26, 2020
2c4dcab
Update golden results.
tjj2017 May 26, 2020
8a75955
Update golden results following rebase to latest diffblue/master.
tjj2017 Jun 4, 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
19 changes: 12 additions & 7 deletions experiments/golden-results/StratoX-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

5 changes: 5 additions & 0 deletions experiments/golden-results/UKNI-Information-Barrier-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
5 changes: 5 additions & 0 deletions experiments/golden-results/ksum-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
10 changes: 5 additions & 5 deletions experiments/golden-results/libkeccak-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
--
Expand All @@ -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
Expand Down
10 changes: 5 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 @@ -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
Expand Down Expand Up @@ -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
Expand Down
5 changes: 0 additions & 5 deletions experiments/golden-results/muen-summary.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
--
Expand Down
Loading