Nondet model #346
Nondet model #346
Conversation
|
A build failure which is probably due to the attempt I made at resolving the merge. A rebase will probably fix this. |
|
@chrisr-diffblue CI seems to have jammed, please can you kick it? |
|
@martin-cs I tried applying the appropriate Size 9 steel toecap, but it looks like the build will (a) need a rebase + force push, and (b) there's an actual compile failure: https://travis-ci.org/github/diffblue/gnat2goto/builds/693545193 |
|
Thanks for the percussive maintenance. @tjj2017 has rebased and forced push it still appears jammed. Any chance of @chrisr-diffblue 's boot vs. CI system round 2? |
|
I've tried kicking it again, but it still seems to fail https://travis-ci.org/github/diffblue/gnat2goto/builds/693545193 and I also note that this PR currently has conflicts. Does the rebased code still build locally for you? |
Intrinsic - A unsupported report is generated for importing a foreign language entity rather than a warning message. No_Corresponding_Spec - pragma Global no longer generates an unsuported report. The pragma has no effect for ASVAT analysis unless it is an ASVAT model when it is used to define the global variables of an interface model.
In the CI tests there are many eaxmples of pragma Import with convention Ada which are not ASVAT models. It might be possible to resolve such instances but since Annotate ASVAT is now the preferred way to specify ASVAT models, it seemed better remove support for specifying via Import. Also this branch included code to check whether an Intrinsic program had a body known to gnat2goto. If this check was to comprehensive it should also check if an Imported subprogram with convention Ada has body known to gnat2goto. After some consideration, it was decided that this should not be checked by gnat2goto but at the link phase. So the Intrinsic check has been removed. Gnat2goto still checks and reports an unsupported node if a called subprogram is not in the symbol table.
Main differences are due to: Now reporting an unsupported node for multi-language imports/exports rather than a warning message. Pragma/aspect Global now acceptrd as a no-op for ASVAT analysis but meaningful for ASVAT modelling. In StratoX a failed precondition in arrays.ads seems to be replaced by an assertion failure in atree.adb. The precondition in arrays.ads is not changed by this mod, so the changes made to the code must now avoid this particular precondition failure but the code then fails later in atree.adb.
|
@chrisr-diffblue I think everything is now working (and building and CIing and mergeable-ing) so I think we are going to declare victory at this point. |
Provide of specifying ASVAT models via an annotation.
Current models are Nondet_Function and In_Type_Function.
See header of ASVAT.Modelling (asvat-modelling.ads).