Robert/automatic ci tests#41
Open
Robert-Brune wants to merge 24 commits intomainfrom
Open
Conversation
— Fix package paths in execution description — Explain development procedure in more detail
- Add `EnclosedExpr` to all arguments of an `BinaryExpr` or `UnaryExpr` - As `jmlparser` needs creates a parse tree, and not a abstract syntax tree, it is better to use braces in all cases, so there are no ambiguities. - #5
Use normal `BinaryExpr` expressions instead of `JmlInfixExpression`. Add enclosed expression for proper encapsulation of arguments.
Robert/bugfix/boolean operator
* Add `result != null` to verifast constructor * Add `result != null` for `out`-arguments - Model logic and reference types in verifast AST - Add proper types for `verifast` - Adapt functions and translations accordingly * Better constructor support for verifast export translations - Extend VeriFast-AST to support constuctors - Intruduction of VeriFastJavaExpressions and VeriFastJavaStatements - Add support of added AST classes in Printer - Simplification of method bodies in blueprints - Fix in Map Example where constructors where ambiguous * Remove `//@Assume false;` from constructor in provider.
Update assemble procedure to support new adapters easily - Simplify build structure - add application in parent (instead of cl subprojcect) - add dependencies of the different adapters to root project - Build -all and -light shadow JAR (with correct manifest files) - Add maven publish to work with the extension (required by extension template) - Use @autoservice to not work with service files manually
When switching to the simplified adapter plugin system, the adapter manifest of the translations was also deleted, leading to crashed. Also fix build scrip for integration tests to find adapters.
- Add SharedContextManager for caching state between adapters - Add ContextProvider and add Picocli interface - Add command class for checker-adapter - Add SharedContexts for: - SourcePaths - ResultDirectory - Add SharedContextProvider for: - SourcePaths - ResultDirectory - Modify Main class to use Picocli - Rework error and info messages to match the design of shared-contexts. - Create a `MessageContext` abstraction that replaces the `ChameleonMessageManager` - First draft of an interface for the `MessageContext` to log messages in a structured way. - Make the `MessageContext` a necessary requirement for the `SharedContextManager`. - All error messages now go over the interface of the `MessageContext`. - The printing of the messages is handed over to the user interface. - Remove 'help' adapter as this is now handled by the `picocli` (user) interface. - Move the Export/Import/Checker Adapter to `adapters` package. - Simplification in the context providers using the improved message context. - First steps to let the `Adapter` abstraction make use of the new context style. - Some documentation. Note: The `MessageContext` still uses the `ChameleonMessageManager` internally, and the `ChameleonMessageManager` is available to the outside. This dependency should be removed in the future. Note: The rework of the `Adapter` interface is not fully completed. Especially, the existing adapters are not adapted to the new interface yet. * Introduce translation adapter, rework result context. - Change the import / export adapter to general translation adapter - Move the directory generation and file writing to the result context (from the adapter). This is now generalized over all adapters. - Make the existing adapters use the new context interface. Note: Discuss, additional import / export adapter to reduce code duplication. * Add override mode to integration test config * Add log level - fix spelling from override to overwrite - add log level to picocli interface - use set instead of list in required interface adapters - add initialization step for default contexts in cc command line interface * Fix tests to use overwrite instead of override
* Simplify export adapter, reduce redundancy
Simplify single contract, and minor contract changes - if there is no multi-contract, the complicated contract join is omitted - remove redundant `instance` keyword from class declarations (can be manually enabled) - Improvement of the message for the provider in generated methods needing implementation - Remove accessible from contract returning void - change name footprint -> fp - Add `new_elems_fresh` clause to contract for mutatable footprints
* Update README - Add description of `contract-chameleon` from extension package - Add section about basic terminology - Add description of translation-, checker-, import-, export-, provider-, applicant-adapter - Motivate intension behind the different adapter types - Add graphic for role of `Contract-LIB` in verification. - Add diagram for adapter types and their relation - Add description about the new graphs to README - Restructure section how to run the tool, make explanation more precise - Restructure and extend section how to develop the tool - Update old help adapter to the new interface using arguments
- To supply implementation in integration test pipeline - Create this for the encapsulation example
- Fix in the directory generation for results - Muliple adjustments in the code generation for verifast - Add substitution of result -> this in - Extend printer to allow printing of comments - Add function to define verifast tasks in gradle - Call encapsulation-example applicant in vf - Call encapsulation-example provider in vf (work still needed) - Add replacements for Cell Todo: - The LinkedCellList example is still missing an implementation - The Cell requires the definition of the predicate manually - remove `this` from predicates like in `this.pred(…)`
- Fix wrong variable names, and problems with verifast's predicate identification when using `this` on class owned predicates - Move the created files in the integration to a build folder - Add more comments to be replecable by the integration test - predicate implementation - class body - Add substitutions that where missing (for whatever reason)
- the full encapsulation example can be verified in verifast - provider (20 statements verified) - applicant (0 statements verified, but can be loaded without issues) - change `JSON` replacement file to `TOML` file (better multiline support for string - needed for longer implementations) - extend todo comments in verifast, to allow more automatic code replacement - remove `result != null` postcondition for ref types, as this should not be there by default and if required, should be just added in the ensures condition
Robert-Brune
added
adapter/key/export-provider
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Open Todos
Baisc CI Test setup
VeriFast Adapter (Export)
KeY Adapter (Export)