Bump CBMC submodule and prettify JSON output #118
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
By default, gnatcoll-json will generate 'compact' JSON - i.e. JSON that has no line breaks or indentation. This is tricky to read when debugging. This change tells gnatcoll-json not to compact the JSON output.
The 'Comment' JSON object is only needed in the JSON schema to handle naming of '#' in comment attributes. The final JSON output should contain the comment attributes as part of the 'namedSub' object.
martin-cs
approved these changes
Jan 31, 2019
xbauch
approved these changes
Jan 31, 2019
gnat2goto/driver/tree_walk.adb
Outdated
| Element_Type_Ent : constant Entity_Id := Get_Array_Component_Type (N); | ||
| Element_Type : constant Irep := Do_Type_Reference (Element_Type_Ent); | ||
| -- Element_Type_Ent : constant Entity_Id := Get_Array_Component_Type (N); | ||
| -- Element_Type : constant Irep := Do_Type_Reference (Element_Type_Ent); | ||
| StrLen : constant Integer := | ||
| Integer (String_Length (Strval (N))); | ||
| String_Length_Expr : constant Irep := New_Irep (I_Constant_Expr); |
There was a problem hiding this comment.
Technically not, at the moment - but I think it will be again when we finally get types for string literals sorted out. The gnat compiler is happy enough for the moment though as String_Length_Expr gets passed into Set_Type/Set_Value. Happy to comment out these as well if people prefer.
There was a problem hiding this comment.
I've commented out this currently unused code too.
Until we get proper types working for string literals, this change allows cbmc to at least assert equality/inequality between string literals. Even if we had proper array types for strings, until we have arrays working, we can't do much with them - so this is a reasonable halfway house for now.
chrisr-diffblue
force-pushed
the
submodule-bump
branch
from
78ade79 to
eeb69f5
Compare
|
All fine with me. |
|
Correction : please check the CI results; esp. the regression tests for packages. |
|
@martin-cs - I'm not seeing any test failures other than things that are XFAILED: |
|
This is the CI build from before the submodule bump: https://travis-ci.org/diffblue/gnat2goto/builds/485435139 |
|
OK; these two: so I will merge. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.