diff --git a/.gitlab/issue_templates/bug_report.md b/.gitlab/issue_templates/bug_report.md
new file mode 100644
index 0000000000000000000000000000000000000000..b01c0a798eea16182a8c10988dd03d4c870a5e32
--- /dev/null
+++ b/.gitlab/issue_templates/bug_report.md
@@ -0,0 +1,35 @@
+Thank you for submitting an issue to the Frama-C team.
+We propose the following template to ease the process.
+Please directly edit it inline to provide the required information.
+
+Before submitting the issue, please confirm (by adding a X in the [ ]):
+
+- [ ] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
+- [ ] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
+- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
+
+# Contextual information
+
+- Frama-C installation mode: *Opam, Homebrew, package from distribution, from source, ...*
+- Frama-C version: *Frama-C version* (as reported by `frama-c -version`)
+- Plug-in used: *Plug-in used*
+- OS name: *OS name*
+- OS version: *OS version*
+
+*Please add specific information deemed relevant with regard to this issue.*
+
+# Steps to reproduce the issue
+
+*Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.*
+
+# Expected behaviour
+
+*Please explain here what is the expected behaviour.*
+
+# Actual behaviour
+
+*Please explain here what is the actual (faulty) behaviour.*
+
+# Fix ideas
+
+*Please tell us if you already tried some work-arounds or have some ideas to solve this issue.*
diff --git a/.gitlab/merge_request_templates/external_contribution.md b/.gitlab/merge_request_templates/external_contribution.md
new file mode 100644
index 0000000000000000000000000000000000000000..e7586d07962708f8e7abec8c04a7f8223a3291f7
--- /dev/null
+++ b/.gitlab/merge_request_templates/external_contribution.md
@@ -0,0 +1,9 @@
+Thank you for submitting a merge request to the Frama-C team.
+We propose the following template to ease the process.
+Please directly edit it inline to provide the required information.
+
+Before submitting the merge request, please confirm (by adding a X in the [ ]):
+
+- [ ] you contributed to Frama-C as prescribed in the [instructions](CONTRIBUTING.md).
+- [ ] if the size of the PR requires it, you have signed the
+ [Contributor Licensing Agreement](CLA.md)
diff --git a/CLA.md b/CLA.md
new file mode 100644
index 0000000000000000000000000000000000000000..7ecfa70238427e38c1f86c7fba9a3744c2d428cb
--- /dev/null
+++ b/CLA.md
@@ -0,0 +1,234 @@
+---
+geometry:
+- top=15mm
+- bottom=15mm
+- margin=10mm
+---
+Contributor Agreement
+=====================
+
+Thank you for your interest in contributing to Frama-C, distributed by
+the Commissariat à l'Energie Atomique et aux Energies Alternatives
+(\"We\" or \"Us\").
+
+The purpose of this Contributor Non-Exclusive License Agreement
+(\"Agreement\") is to clarify and document the rights granted by
+contributors to Us. To make this document effective and get started,
+please sign the Contributor License Agreement.
+
+Please read this document carefully before signing and keep a copy for
+your records.
+
+**1. DEFINITIONS**
+
+**\"You\" (/"Your")**Â means the Individual Copyright owner or Entity as
+defined hereunder who submits a Contribution to Us. If You are an
+employee and submit the Contribution as part of your employment, You
+represent that you have the authority and/or required authorization in
+binding the Entity to this Agreement, and to sign this version of this
+document. In such case "You" (/"Yours") shall refer to such Entity.
+
+**\"Documentation\"**Â means any non-software portion of a Contribution.
+
+**"Entity"** shall mean the copyright owner or legal entity (including
+but not limited to any institution, company, corporation, partnership,
+government agency or university) authorized by the copyright owner that
+is making this Agreement with Us and all other entities that control,
+are controlled by, or are under common control with that entity are
+considered to be a single Contributor. For the purposes of this
+definition, \"control\" means (i) the power, direct or indirect, to
+cause the direction or management of such entity, whether by contract or
+otherwise, or (ii) ownership of fifty percent (50%) or more of the
+outstanding shares, or (iii) beneficial ownership of such entity.
+
+**\"Contribution\"**Â means any original work of authorship (software
+and/or documentation) including any modifications or additions to an
+existing work, Submitted by You to Us, in which You own the Copyright.
+
+**\"Copyright\"**Â means all rights protecting works of authorship owned
+or controlled by You, including copyright, moral and neighboring rights,
+as appropriate, for the full term of their existence including any
+extensions by You.
+
+**\"Submit\"**Â means any form of physical, electronic, or written
+communication sent to Us, including but not limited to electronic
+mailing, source code control systems, and issue tracking systems that
+are managed by, or on behalf of, Us, but excluding communication that is
+clearly designated in writing by You as \"Not a Contribution.\"
+
+\"**Work**\" means any software or documentation made available by Us to
+third parties. Any Contribution You Submit may be included in the
+Material.
+
+**2. GRANT OF LICENSE**
+
+> **2.1 Grant of Copyright License.**
+
+Subject to the terms and conditions of this Agreement, You hereby grant
+to Us a worldwide, royalty-free, no-charge, non-exclusive, perpetual and
+irrevocable Copyright license, with the right to transfer an unlimited
+number of non-exclusive licenses or to grant non-exclusive sublicenses
+to third parties, to use the Contribution by all means, including but
+not limited to, the right to :
+
+- Publish the Contribution in original or modified form ;
+
+- Modify the Contribution, prepare derivative works based upon or
+ containing the Contribution and combine the Contribution with other
+ works;
+
+- Reproduce the Contribution in original or modified form;
+
+- Distribute, make the Contribution available to the public, display
+ and publicly perform the Contribution in original or modified form
+ under the terms of any license approved by Us.
+
+> **2.2 Moral Rights**
+
+Moral Rights remain unaffected to the extent they are recognized and not
+waivable by applicable law. Notwithstanding, You may add your name in
+the header of the source code files of Your Contribution and We will
+respect this attribution when using Your Contribution.
+
+**3. GRANT OF PATENT LICENSE**
+
+Subject to the terms and conditions of this Agreement, You hereby grant
+to Us a perpetual, worldwide, non-exclusive, no-charge, royalty-free,
+irrevocable patent license, with the right to transfer an unlimited
+number of non-exclusive licenses or to grant sublicenses to third
+parties, to make, have made, use, offer to sell, sell, import, and
+otherwise transfer the Contribution, where such license applies only to
+those patent claims licensable by You that are necessarily infringed by
+Your Contribution(s) alone or by combination of Your Contribution(s)
+with the Work to which such Contribution(s) was submitted.
+
+This license applies to all patents owned or controlled by You, whether
+already acquired or hereafter acquired, that would be infringed by
+making, having made, using, selling, offering for sale, importing or
+otherwise transferring of Your Contribution(s) alone or by combination
+of Your Contribution(s) with the Material.
+
+You furthermore agree to notify Us of any patents that you know or come
+to know which are likely infringed by the Contribution and/or are not
+licensable by You.
+
+If any entity institutes patent litigation against You or any other
+entity alleging that the Contribution, or the Work with which it has
+been combined, constitutes direct or contributory patent infringement,
+then any patent licenses granted to that entity under this Agreement for
+that Contribution or Material shall terminate as of the date such
+litigation is filed.
+
+If the litigation is withdrawn or otherwise settled, then any patent
+licenses granted to that entity under this agreement shall be reinstated
+as of the date the litigation was settled or withdrawn.
+
+**4. REPRESENTATIONS**
+
+a\. If You are entering this Agreement as an individual, You represent
+that You are legally entitled to grant the licenses set forth in
+Sections 2 and 3. If Your employer(s) has rights to intellectual
+property that You create, such as your Contributions, You represent that
+You have received permission to make Contributions on behalf of that
+employer and that Your employer has waived such rights for Your
+Contributions to the Work.
+
+b\. If You are entering this Agreement on behalf of an Entity, You
+represent that You are legally entitled to grant the licenses set forth
+in Sections 2 and 3 and that each employee of the Entity that submits
+Contributions is authorized to submit such Contributions on behalf of
+the Entity.
+
+In any case, You represent that:
+
+i\. The Contribution is Your original creation. If You do not, entirely
+or partially, own the Copyright in work of authorship comprising a
+Contribution, please contact Us before Submitting such Contribution.
+
+ii\. to the extent that Your Contribution is computer code, it includes
+complete details of any third-party license or other restriction
+(including, but not limited to, related patents and trademarks) of which
+You are personally aware and which are associated with any part of Your
+Contributions.
+
+iii\. to the extent that Your Contribution is computer code, it contains
+no viruses, Trojan horses, backdoors, malicious code or other program
+that would allow anyone, including Us, to gain access to a computer or
+network other than what is fully documented and disclosed by Us.
+
+**5. DISCLAIMER OF WARRANTIES**
+
+Except as set forth in section 4, the contribution is provided \"as
+is\". More particularly, all express or implied warranties including,
+without limitation, any implied warranty of merchantability, fitness for
+a particular purpose and non-infringement are expressly disclaimed by
+You to Us and by Us to You. To the extent that any such warranties
+cannot be disclaimed, such warranty is limited in duration to the
+minimum period permitted by law.
+
+**6. CONSEQUENTIAL, APPROXIMATION OF DISCLAIMER AND DAMAGE WAIVER**
+
+To the maximum extent permitted by applicable law, in no event will You
+or Us be liable for any loss of profits, loss of anticipated savings,
+loss of data, indirect, special, incidental, consequential and exemplary
+damages arising out of this Agreement regardless of the legal or
+equitable theory (contract, tort or otherwise) upon which the claim is
+based.
+
+If the disclaimer and damage waiver mentioned in section 5 and section 6
+cannot be given legal effect under applicable local law, reviewing
+courts shall apply local law that most closely approximates an absolute
+waiver of all civil liability in connection with the contribution.
+
+**7. TERM**
+
+This Agreement shall come into effect upon Your acceptance of the terms
+and conditions.
+
+In the event of a termination of this Agreement Sections 5, 6 and 8
+shall survive such termination and shall remain in full force
+thereafter. For the avoidance of doubt, Contributions that are already
+licensed under a free and open source license at the date of the
+termination shall remain in full force after the termination of this
+Agreement.
+
+**8. MISCELLANEOUS**
+
+8.1 You are not expected to provide support for Your Contributions,
+except to the extent You desire to provide support. You may provide
+support for free, for a fee, or not at all. Unless required by
+applicable law or agreed to in writing, You provide Your Contributions
+on an \"as is\" basis, without warranties or conditions of any kind,
+either express or implied, including, without limitation, any warranties
+or conditions of title, non-infringement, merchantability, or fitness
+for a particular purpose.
+
+8.2 This Agreement and all disputes, claims, actions, suits or other
+proceedings arising out of this agreement or relating in any way to it
+shall be governed by the laws of France excluding its private
+international law provisions.
+
+8.3 This Agreement sets out the entire agreement between You and Us for
+Your Contributions to Us and overrides all other agreements or
+understandings.
+
+8.4 If any provision of this Agreement is found void and unenforceable,
+such provision will be replaced to the extent possible with a provision
+that comes closest to the meaning of the original provision and that is
+enforceable. The terms and conditions set forth in this Agreement shall
+apply notwithstanding any failure of essential purpose of this Agreement
+or any limited remedy to the maximum extent possible under law.
+
+8.5 You agree to notify Us of any facts or circumstances of which you
+become aware that would make this Agreement inaccurate in any respect.
+
+**Signature**
+
+- Full Name:
+- Entity (if applicable):
+- Country/Town:
+- (optional) Full address:
+- Email:
+- Gitlab login:
+- Date:
+- Signature:
diff --git a/CLA.pdf b/CLA.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..c3435b49a207be715c8a67b45c2d28eec39c2e37
Binary files /dev/null and b/CLA.pdf differ
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000000000000000000000000000000000000..5c3a674ee5aca48c0a5f864812cad2aafe461e0b
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,152 @@
+Contributing to Frama-C
+=======================
+
+We always welcome technical as well as non-technical contributions from the
+community.
+There are several ways to participate in the Frama-C project:
+
+- Asking questions and discussing at
+ [StackOverflow](https://stackoverflow.com/tags/frama-c) and through
+ the
+ [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss);
+
+- Reporting bugs via
+ [Gitlab issues](https://git.frama-c.com/pub/frama-c/issues);
+
+- [Submitting bug fixes, improvements and features](#submitting-bug-fixes-improvements-and-features)
+ via Gitlab merge requests;
+
+- [Developing external plug-ins](#developing-external-plug-ins)
+ and sharing it with us through a Gitlab merge request;
+
+- Joining the [Frama-C team](http://frama-c.com/about.html) (as an intern, a PhD
+ student, a postdoctoral researcher, or a research engineer).
+
+We give below some guidelines in order to ease the submission of a merge request
+and optimize its integration with the Frama-C existing codebase.
+
+
+Submitting bug fixes, improvements, and features
+================================================
+
+External contributions can be proposed via the
+public Frama-C gitlab [repository](https://git.frama-c.com/pub/frama-c),
+by following the recommended workflow in git development:
+fork the frama-c repository, develop in a dedicated branch
+and submit a merge request.
+
+The detailed steps to submit a contribution to Frama-C are:
+
+1. If you plan to make a significant contribution to Frama-C, please
+ [open an issue](https://git.frama-c.com/pub/frama-c/issues/new)
+ describing your ideas, to discuss it with the Frama-C development team.
+
+2. [Fork the public Frama-C repository](https://git.frama-c.com/pub/frama-c/-/forks/new)
+ (choosing your Gitlab account as a destination);
+
+3. Clone the forked Frama-C snapshot repository on your computer;
+
+4. Create and switch to a dedicated branch. We suggest the following
+ naming convention:
+ - `fix/short-description` for bug fixes (correcting an incorrect
+ behavior);
+ - `feature/short-description` for features (adding a new behavior).
+
+5. Locally make your contribution by adding/editing/deleting files and following
+ the [coding conventions](#coding-conventions);
+
+6. (Optional) Locally add non-regression test cases to the appropriate
+ subdirectory in `./tests/`. The `hello` tutorial in the
+ [plug-in developer manual](http://frama-c.com/download/frama-c-plugin-development-guide.pdf)
+ provides an example of the use of the dedicated `ptests`
+ tool used by Frama-C developers. The full documentation for `ptests` is also
+ present later in the same manual.
+ You can also provide the non-regression test case in the Gitlab issue
+ discussion and we will integrate it.
+
+7. Check for unexpected changes.
+ Use the command `make lint`
+ in your terminal from the Frama-C root directory to detect trailing spaces,
+ tabulations or incorrect indentation (ocp-ident >= 1.7.0 is needed).
+
+8. Locally run the test framework of Frama-C by typing
+ `make tests`
+ in your terminal (you should be in the Frama-C root directory);
+
+9. Locally add (if needed) and commit your contribution;
+
+10. Push your contribution to Gitlab;
+
+11. [Make a Gitlab merge request](https://git.frama-c.com/pub/frama-c/merge_requests).
+ The target should remain as repository `pub/frama-c` and branch `master`
+ while the source should be your personal project and your chosen branch
+ name.
+
+12. If needed (i.e. you didn't already do that and your contribution is
+ not trivial in the sense of [this document](TCA.md)), please don't forget
+ to fill and sign the [Contributor Licence Agreement](CLA.pdf) and send us
+ the signed version at `cla AT frama-c DOT com`
+
+For convenience, we recall the typical `git` commands to be used through these steps:
+```shell
+git clone https://git.frama-c.com/<username>/frama-c.git
+git checkout -b <branch-name>
+git diff --check
+git add <file1 file 2>
+git commit -m "<Commit message>"
+git push origin <branch-name>
+```
+where:
+
+- `<username>` is your Gitlab username;
+- `<branch-name>` is your chosen branch name;
+- `<file1 file2>` are the files to add to the commit;
+- `<Commit message>` is your commit message.
+
+
+Developing external plug-ins
+============================
+
+Frama-C is a modular platform for which it is possible to develop external
+plug-ins as documented in the
+[Plug-In development guide](http://frama-c.com/download/frama-c-plugin-development-guide.pdf).
+Such plug-ins normally do not require changes to the Frama-C source code and can
+be developed completely independently, for instance in a separate Git
+repository as exemplified by the [Hello plug-in](https://github.com/Frama-C/frama-c-hello).
+
+However, to make it easier for your users to compile and use your plug-in, even
+as newer releases are made available, we recommend the following workflow:
+
+1. Write your external plug-in as indicated in the
+ [Plug-In development guide](http://frama-c.com/download/frama-c-plugin-development-guide.pdf);
+
+2. Create an `opam` package by
+ [pinning your local plug-in](http://opam.ocaml.org/doc/Packaging.html#Opam-pin) and
+ [editing the `opam` file](http://opam.ocaml.org/doc/Packaging.html#The-quot-opam-quot-file).
+ You can have a look at the
+ [`opam` file of the Hello plug-in](https://github.com/Frama-C/frama-c-hello/blob/master/opam)
+ if necessary.
+
+3. Optionally
+ [publish your plug-in](http://opam.ocaml.org/doc/Packaging.html#Publishing)
+ in the official OPAM packages repository.
+
+4. Announce your contribution to the Frama-C ecosystem on the
+ [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss).
+ Well done!
+
+The main advantage of this procedure is that opam will perform several
+consistency checks of your plug-in,
+with respect to several Frama-C versions and OCaml dependencies.
+
+Coding conventions
+==================
+
+- Use [ocp-indent](https://github.com/OCamlPro/ocp-indent), v1.7.0
+ to indent OCaml source files;
+
+- Avoid trailing whitespaces;
+
+- Avoid using tabs;
+
+- Strive to keep within 80 characters per line.
diff --git a/Changelog b/Changelog
index e45deb4ca12e5fdc584f69602199f5b7a39dfe5b..22925cf250a87b8d0d3c568c12d20fdf606b08ea 100644
--- a/Changelog
+++ b/Changelog
@@ -21,10 +21,15 @@ Open Source Release <next-release>
Open Source Release 20.0 (Calcium)
####################################
+- Eva [2019/11/25] In the summary, fixes the number of alarms by
+ category when the RTE plugin is used, and do not count logical
+ properties in dead code as proven.
-! Kernel [2019/10/31] More stringent verifications on the use of ghost
variable in non ghost-code. Fixes #2421
- MdR [2019/10/31] New plug-in Markdown-Report (MdR) for markdown and
SARIF outputs
+- Eva [2019/10/23] In the summary, fixes the total number of functions
+ (and thus the computed analysis coverage).
- Eva [2019/10/23] New option -eva-auto-loop-unroll N to unroll all
loops whose number of iterations can be easily bounded by <N>.
- Eva [2019/10/21] New octagon domain inferring relations of the form
diff --git a/TCA.md b/TCA.md
new file mode 100644
index 0000000000000000000000000000000000000000..7c28ab8e534241bbb31c4c73657a7b2ee189b0b0
--- /dev/null
+++ b/TCA.md
@@ -0,0 +1,78 @@
+**Trivial Contribution Policy**
+
+The purpose of this Policy is to clarify and document the circumstances
+in which a Contribution, deemed as Trivial, does not fall within the
+scope of the Contributor License Agreement.
+
+As a general rule, Contributions that do not involve creative decisions
+or which are not substantial will be considered to be Trivial.
+
+As a guideline, a Contribution may be qualified according to the
+following:
+
++-----------------------+-----------------------+-----------------------+
+| *Type of | *≤ 10 lines* | *\> 10 lines* |
+| contribution* | | |
++=======================+=======================+=======================+
+| Feature | | |
+| | • Not trivial | • Not trivial |
+| (add new functional | | |
+| behavior) | | |
++-----------------------+-----------------------+-----------------------+
+| Improvement | | |
+| | • Probably | • Not trivial |
+| (improve | not trivial | |
+| non-functional | | |
+| behavior) | | |
++-----------------------+-----------------------+-----------------------+
+| | • Not trivial if | • Not trivial if |
+| | creative code | creative code |
+| Bug fix | | |
+| | • Not trivial if | • Not trivial if |
+| (fix incorrect | comprises a creative | comprises a creative |
+| behavior) | comment | comment |
+| | | |
+| | • Probably trivial | • Probably not |
+| | otherwise | trivial otherwise |
++-----------------------+-----------------------+-----------------------+
+
+(1) - - -
+
+<!-- -->
+
+(1)
+
+Without prejudice to the above, and for all intents and purposes, the
+following Contributions are deemed to be Trivial:
+
+- Spelling / grammar fixes / correcting typos
+
+- Formatting / cleaning up comments in the code.
+
+- Contributions that are purely deletions, such as removal of
+ duplicate information or code that never executes.
+
+- Bug fixes that change default return values or error codes stored in
+ constants, literals, or simple variable types.
+
+- Adding logging messages or debugging output.
+
+- Changes to 'metadata' files.
+
+- Renaming a build directory or changing a constant.
+
+- Configuration changes.
+
+- Changes in build or installation scripts.
+
+- Re-ordering of objects or subroutines.
+
+- Moving source files from one directory or package to another, with
+ no changes in code.
+
+- Breaking a source file into multiple source files, or consolidating
+ multiple source files into one source file, with no code changes.
+
+However, there are many gray areas. Please reach us at `cla AT frama-c DOT com`
+should you have any questions on the nature of your
+intended Contribution.
diff --git a/src/plugins/e-acsl/src/code_generator/visit.ml b/src/plugins/e-acsl/src/code_generator/visit.ml
index 24a2372bf75a27e1869d40ad7da49b9fb2fe3c31..93874cf54d70b93973d5148cfda0a832c38cd746 100644
--- a/src/plugins/e-acsl/src/code_generator/visit.ml
+++ b/src/plugins/e-acsl/src/code_generator/visit.ml
@@ -487,11 +487,22 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| g when Misc.is_library_loc (Global.loc g) ->
if generate then Cil.JustCopy else Cil.SkipChildren
| g ->
+ let unghost_vi vi =
+ vi.vghost <- false ;
+ vi.vtype <- match vi.vtype with
+ | TFun(res, Some l, va, attr) ->
+ let retype (n, t, a) =
+ (n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a)
+ in
+ TFun(res, Some (List.map retype l), va, attr)
+ | _ ->
+ vi.vtype
+ in
let do_it = function
| GVar(vi, _, _) ->
- vi.vghost <- false
+ unghost_vi vi
| GFun({ svar = vi } as fundec, _) ->
- vi.vghost <- false;
+ unghost_vi vi ;
Builtins.update vi.vname vi;
(* remember that we have to remove the main later (see method
[vfile]); do not use the [vorig_name] since both [main] and
@@ -502,7 +513,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* do not convert extern ghost variables, because they can't be linked,
see bts #1392 *)
if vi.vstorage <> Extern then
- vi.vghost <- false
+ unghost_vi vi
| _ ->
()
in
@@ -594,7 +605,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if Functions.instrument kf then Exit_points.generate f;
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
+ let unghost_formal vi =
+ vi.vghost <- false ;
+ vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr
+ in
List.iter (fun vi -> vi.vghost <- false) f.slocals;
+ List.iter unghost_formal f.sformals;
Cil.DoChildrenPost
(fun f ->
Exit_points.clear ();
diff --git a/src/plugins/e-acsl/tests/memory/ghost_parameters.i b/src/plugins/e-acsl/tests/memory/ghost_parameters.i
new file mode 100644
index 0000000000000000000000000000000000000000..a3577b57397f410c825ff1529b6166fbb4d2a52b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/ghost_parameters.i
@@ -0,0 +1,17 @@
+/* run.config
+ COMMENT: ghost parameters
+ STDOPT:
+*/
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+int main(void){
+ int w = 0 ;
+ int x = 1 ;
+ //@ ghost int y = 2 ;
+ //@ ghost int z = 3 ;
+
+ function(w, x) /*@ ghost(y, z) */;
+}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
new file mode 100644
index 0000000000000000000000000000000000000000..21e0d8d49e93362922685b0c1538a1026d24bedf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -0,0 +1,22 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+void function(int a, int b, int c, int d)
+{
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int w = 0;
+ int x = 1;
+ int y = 2;
+ int z = 3;
+ function(w,x,y,z);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 7f1f0f1a35815877a55c4a4cbc9d9f9a4effebeb..517f9857173e4c91d9fcb76e029d08d280b7ce11 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -223,6 +223,7 @@ sig
val pool : ?copy:pool -> unit -> pool
val fresh : pool -> ?basename:string -> tau -> var
+ val alpha : pool -> var -> var
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 1b95285882dde1a81db416d4eb23ac4b1537fa58..2cba2c899f7ba69309810d33649ca10ffa297a04 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -130,8 +130,8 @@ let bind ~side bindings property : Tactical.process =
let open Conditions in
instance_have ?title:s.descr ~at:s.id bindings property
-let filter x e =
- try F.Tau.equal (F.tau_of_var x) (F.typeof e)
+let filter tau e =
+ try F.Tau.equal tau (F.typeof e)
with Not_found -> true (* allowed to not restrict usage *)
let fieldname ~range k x =
@@ -159,7 +159,7 @@ class instance =
let range = match tau with L.Int -> true | _ -> false in
let tooltip = fieldname ~range env.index x in
env.feedback#update_field
- ~tooltip ~range ~enabled:true ~filter:(filter x) fd ;
+ ~tooltip ~range ~enabled:true ~filter:(filter tau) fd ;
let lemma = F.QED.e_unbind x phi in
let bindings,property = self#wrap env lemma fields in
(x,v) :: bindings , property
diff --git a/src/plugins/wp/TacInstance.mli b/src/plugins/wp/TacInstance.mli
index 46e523c1676e82d938b9e0bea9b1c5ba6871127b..00d5adfe2c1df87a551cd3ed6acfe50d0d0b05b6 100644
--- a/src/plugins/wp/TacInstance.mli
+++ b/src/plugins/wp/TacInstance.mli
@@ -29,7 +29,7 @@ open Strategy
val tactical : Tactical.t
val fields : selection field list
val params : parameter list
-val filter : var -> term -> bool
+val filter : tau -> term -> bool
type bindings = (var * selection) list
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index 343dbe4ffb0a2d90ae354604162b821c96e81ba4..3f24df008655edc83a529553a9c985c01f38c55b 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -90,6 +90,12 @@ let search,psearch =
Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to Instantiate"
~browse ~find:Definitions.find_name ()
+
+let fresh pool { l_forall ; l_lemma } =
+ let vars = List.map (F.alpha pool) l_forall in
+ let sigma = Lang.subst l_forall (List.map F.e_var vars) in
+ vars , F.p_subst sigma l_lemma
+
class instance =
object(self)
inherit Tactical.make ~id:"Wp.lemma"
@@ -111,7 +117,7 @@ class instance =
env.feedback#update_field ~enabled:true
~title ~tooltip:env.descr
~range:(match tau with L.Int -> true | _ -> false)
- ~filter:(TacInstance.filter x) fd ;
+ ~filter:(TacInstance.filter tau) fd ;
let bindings,lemma = self#wrap env xs fields in
(x,value)::bindings , lemma
| _ ->
@@ -125,17 +131,16 @@ class instance =
| None ->
self#hide feedback TacInstance.fields ;
Not_configured
- | Some l ->
- let descr = l.Tactical.descr in
- let lemma = l.value.l_lemma in
+ | Some Tactical.{ title ; value = dlem } ->
+ let fields = TacInstance.fields in
+ let vars,lemma = fresh feedback#pool dlem in
+ let descr = Pretty_utils.to_string F.pp_pred lemma in
let bindings,lemma =
- self#wrap { feedback ; descr ; lemma }
- l.value.l_forall TacInstance.fields in
+ self#wrap { feedback ; descr ; lemma } vars fields in
match TacInstance.cardinal 1000 bindings with
| Some n ->
if n > 1 then
feedback#set_descr "Generates %d instances" n ;
- let title = l.title in
let at = Tactical.at selection in
Applicable
(TacInstance.instance_have ~title ?at bindings lemma)
diff --git a/src/plugins/wp/tests/wp_tip/TacNOP.ml b/src/plugins/wp/tests/wp_tip/TacNOP.ml
index e1c80aa18088963cef7dd67169e56ae1977ffe63..85710ca2329912066d9865231388bc3c2b991f1b 100644
--- a/src/plugins/wp/tests/wp_tip/TacNOP.ml
+++ b/src/plugins/wp/tests/wp_tip/TacNOP.ml
@@ -47,6 +47,5 @@ class nop =
end
let tactical = Wp.Tactical.export (new nop)
-let _ = Wp.Strategy.make tactical ~arguments:[]
(* -------------------------------------------------------------------------- *)