When a source location points to a file that is not part of the session,
the IDE now displays it in an extra tab. If the source locations are
properly positioned, then the source positioning and coloring should
work in these extra files. This feature should be useful for front-ends
generating mlw files with being recorded as a language plug-in
IN an effort to clean up the generated mlw, we remove duplicate
includes. We do this by transforming the includes in an intermediate
representation which can be easily be compared, then use a set to
avoid duplicates. We do this in a way as to preserve ordering of the
includes, as why3 is apparently sensitive to that.
* gnat_ast_to_ptree.ml
(Include_Decl): new module to be able to build sets of includes
(mk_theory_declaration): build a set of includes before translation,
to avoid duplicates
Change-Id: Ibd06f7b7edfe3c55ed5e467837c7f021d17e052e
* gnat_ast.ml: autogenerated
* gnat_ast_to_ptree.ml: remove code for case that's not possible any
more
Change-Id: I0cdc2d90f3fe24dec16ca3a53a83e0a604ecfd9b
This has the following benefits:
- fractional real numbers no longer have spurious zeros;
- hexadecimal real numbers now decay to decimal ones;
- integer real numbers no longer use a multiplication.
This adds the support for 80-bits so-called extended floating-point types
to the IEEE theory of floats in Why3.
[changelog]
* drivers/smt-libv2-floats.gen:
(ieee_float.Float80): Use native support and remove propositions.
(ieee_float.FloatConverter): Remove propositions on this generic theory.
(ieee_float.Float32_64_Converter): Adapt from previous binding.
(ieee_float.Float80_BV_Converter): Similar to other BV converters.
* plugins/gnat_json/gnat_ast_to_ptree.ml: Adapt to new Float80 theory.
* stdlib/ieee_float.mlw:
(Float80): New module.
(FloatConverter): Make module abstract in small/large fp types.
(Float32_64_Converter): New name for previous FloatConverter.
(Float32_80_Converter): New conversion module.
(Float64_80_Converter): New conversion module.
(Float_BV_Converter): Delay axiom of_ubv64_to_real at instantiation.
(Float32_BV_Converter): Provide axiom for of_ubv64_to_real.
(Float64_BV_Converter): Provide axiom for of_ubv64_to_real.
(Float80_BV_Converter): New conversion module.
Change-Id: I8feba3c3440878c4a6a20c511b86b8cd69eef328
When generating the assertion comparing the old value of the variant
with the new one, we were directly using the expression provided in
the Variant node of the GNAT AST. This is not correct, as it may be
a program expression, so not suitable for an assertion. We introduce
let-bindings to introduce temps for these expressions.
* gnat_ast_pretty.ml
new pretty printing functions to (almost) complete pretty-printing
of nodes
* gnat_ast_to_ptree.ml
(mk_of_expr): introduce temps for new values of variants
Change-Id: Ifeb30d508ec834ddf0253c19859f5305fe18d8a5
Normally, result values of function calls are requested during
giant-step RAC by their location. However, lexical, unique locations
can be overwritten using location annotations, which are frequent in
SPARK-generated WhyML programs, resulting in ambiguous locations, and
retrieval of the wrong result values.
As a workaround, this change generates call ids for calls and abstract
expressions, to identify result values in the counterexample uniquely.
In the future, result values should instead be identified by their
structural position in the WhyML AST, to avoid the need for generating
the call ids.
Change-Id: Id4734dc26e0cbdc19289ddeb72f8ec3a42c735f6
OCaml warns when there is a .ml file but no .mli file. This commit adds
almost all the missing .mli files. The remaining ones are the *_ast.ml
files, as the .mli files would be verbatim copies.
