Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
68cb1a45
Commit
68cb1a45
authored
Nov 04, 2012
by
MARCHE Claude
Browse files
Jessie3: integer constants using Why3 protecting constructors
parent
16692122
Changes
3
Hide whitespace changes
Inline
Side-by-side
ROADMAP
View file @
68cb1a45
...
...
@@ -63,11 +63,6 @@
- commentaires dans les sessions, attachés a chaque ligne
=========== Middle-term roadmap ==========================================
* replayer
** deplacer option -bench dans une commande de why3session
* Projets interessant Cesar ?
** Preuve de prog flottants avec Frama-C+WP+Why3+PVS
** Generation d'annotations
...
...
@@ -77,6 +72,65 @@
** support de Yices 2 ? interesserait Cesar
==================== Roadmap for release 0.81 ========================
scheduled on ? 2012
== New Features to announce ==
== Final preparation ==
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate" is OK
(see below : copy the dtd on the web)
* put 0.80 in file Version
* check headers
* check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
* manual in HTML: "make doc/html/index.html"
* do "make distrib"
* test the distrib why3-0.81.tar.gz
* make a last commit:
- add tag 0.81 to the git repository, using git tag 0.81
- do not forget to push it using git push --tags
* install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository
~filliatr/ARCHIVE/www/why)
* put on the web page
- why3-0.81.tar.gz
- the HTML version of the manual (content of doc/html)
- why3session.dtd
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
make stdlibdoc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.81
rm /users/www-perso/projets/why3/stdlib)
ln -s /users/www-perso/projets/why3/stdlib-0.81 \
/users/www-perso/projets/why3/stdlib
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
make apidoc
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.81
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.81 \
/users/www-perso/projets/why3/api
PROBLEME avec style.css
- update the main HTML page (sources are in why3-papers/www)
* produce the Why3 part of ProVal gallery
-> add also a tar.gz and a ZIP file of it (this is done by doing
"make gallery-files" in the sources of the web pages)
* Announce the distrib
- What to put in the announcement: see New Features above
* The next commit : add +git to the version in file Version
== TODOs ==
* replayer
** deplacer option -bench dans une commande de why3session
* extraction vers Caml
- PRIORITAIRE, JCF, ANDREI
...
...
@@ -113,10 +167,21 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
NEED FEEDBACK which ones ???
feeback: it is a conflict with a language file for alt-ergo (?)
* faire le menage dans les transformations d'induction : _int _ty
_ty_lex, et DOCUMENTER
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* sessions
** mettre la dtd sur le web et changer l'entête des sessions pour qu'elles
pointent dessus
==================== Roadmap for release 0.80 ========================
...
...
@@ -209,29 +274,20 @@ Bug fixes:
== TODOs ==
* (JCF) reject global "val"s in typing environment for logic decls.
*
DONE
(JCF) reject global "val"s in typing environment for logic decls.
* appliquer les changements de syntaxe des programmes dans la doc : aussi bien dans le tutorial que dans la BNF des manpages
*
DONE
appliquer les changements de syntaxe des programmes dans la doc : aussi bien dans le tutorial que dans la BNF des manpages
* faire le menage dans les transformations d'induction : _int _ty
_ty_lex, et DOCUMENTER
* Sortie PVS
** avec mecanisme de realization
* DONE Sortie PVS, avec mecanisme de realization
* DONE mettre au propre les loc des fichiers de sessions, en particulier
les noms de fichiers doivent etre relatifs au fichier de session
lui-meme. Utiliser Sysutil.relativize_filename a bon escient.
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* DONE sessions: mettre la dtd sur le web et changer l'entête des sessions pour qu'elles
pointent dessus
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* DONE (PRIORITAIRE) Coq output
- corriger l'incoherence, comprendre si on veut vraiment accepter
...
...
@@ -240,7 +296,7 @@ Bug fixes:
(cf: en caml cela ne marche pas)
Solution proposee: utiliser des types classes, en particulier Inhabited
* DONE
?
PRIORITAIRE, JCF et ANDREI, clone de module
* DONE
(
PRIORITAIRE
)
, JCF et ANDREI, clone de module
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
- cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
...
...
src/jessie/ACSLtoWhy3.ml
View file @
68cb1a45
...
...
@@ -10,6 +10,7 @@
(********************************************************************)
let
help
=
"Checks ACSL contracts using Why3"
let
global_logic_decls_theory_name
=
"Global logic declarations"
...
...
src/jessie/literals.mll
View file @
68cb1a45
...
...
@@ -56,11 +56,11 @@ let oct_escape = '\\' rO rO? rO?
(* integer literals, both decimal, hexadecimal and octal *)
rule
integer_literal
=
parse
(* hexadecimal *)
|
'
0
'
[
'
x''X'
]
(
rH
+
as
d
)
rIS
eof
{
Term
.
IC
onst
H
exa
d
}
|
'
0
'
[
'
x''X'
]
(
rH
+
as
d
)
rIS
eof
{
Term
.
int_c
onst
_h
exa
d
}
(* octal *)
|
'
0
'
(
rO
+
as
d
)
rIS
eof
{
Term
.
IC
onst
O
ctal
d
}
|
'
0
'
(
rO
+
as
d
)
rIS
eof
{
Term
.
int_c
onst
_o
ctal
d
}
(* decimal *)
|
(
rD
+
as
d
)
rIS
eof
{
Term
.
IC
onst
D
ecimal
d
}
|
(
rD
+
as
d
)
rIS
eof
{
Term
.
int_c
onst
_d
ecimal
d
}
(* TODO: character literals
| ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'"
{
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment