jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity
1195 commits 2 branches 0 tags 6.9 MiB
Commit graph

1195 commits

This branch
This branch
All branches
Author SHA1 Message Date
Gwenaël Delaval
2d96b60c49 Bug corrections in contracts 
Contracts handling : added variables for assume/guarantee
parts of subnodes as defined names in b_defnames
 2014-01-27 00:26:24 +01:00
Gwenaël Delaval
1a373b84eb Added some tests 
Tests from image_filters
Examples of array iterators used
 2014-01-15 00:07:29 +01:00
Gwenaël Delaval
c61e01f19b Correct handling of comparison operators in Sigali 
- bug fix: comparison between two non-constant integer expressions in Sigali
 - bug fix: correct handling of "=" and "<>" operators in Sigali
 2014-01-14 23:09:22 +01:00
Nicolas Berthier
4f7413282e Merge branch 'decade' into ctrl-n 2013-11-26 18:03:54 +01:00
Nicolas Berthier
c132b53732 Handle `when' operators in general expressions, in Controllable-Nbac backend. 
- CtrlNbacGen: ignore sub-sampling in general expressions.
 2013-11-26 18:03:07 +01:00
Nicolas Berthier
934c9f9a85 Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend. 2013-11-20 12:13:01 +01:00
Gwenaël Delaval
d27db41485 Version 1.00.03 2013-11-20 10:20:35 +01:00
Nicolas Berthier
808b9772f3 Merge branch 'decade' into ctrl-n 2013-11-20 08:53:00 +01:00
Gwenaël Delaval
71497a82b2 Corrected bug in inline_extvalues 
Inline_extvalues: added local variables of contracts into environments
 2013-11-19 20:39:01 +01:00
Nicolas Berthier
ae6a3aac2e Attractivity property of Controllable-Nbac output; minor refactorings. 2013-11-13 15:35:15 +01:00
Nicolas Berthier
216550c0d1 Fixed warnings & documentation comments. 
- gitignore: ignore files generated by `configure' script.
 2013-11-08 18:51:06 +01:00
Nicolas Berthier
10bdab4dc6 Exclusively use ocamlfind; source documentation generation. 
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
  when `-use-ocamlfind' is passed to ocamlbuild.

- Added some code in `myocamlbuild_config.ml' to be able to generate
  documentation by merging interface and implementation files.
 2013-11-08 15:50:36 +01:00
Nicolas Berthier
8aeab651ce First draft for Controllable-Nbac format generation. 
- CtrlNbac: new module for internal representation and output code for
  Controllable-Nbac format;

- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
  necessitating controller synthesis; the insertion of calls to
  controllers is not yet done, and the nodes are left unchanged.
 2013-11-08 15:13:39 +01:00
Gwenaël Delaval
106b1339ac Corrected Makefile for binary distribution 2013-11-04 11:52:46 +01:00
Gwenaël Delaval
5b98f9cdf6 Version 1.00.02 
Added CHANGES file
 2013-10-29 19:03:31 +01:00
Gwenal Delaval
13d616c930 Scrollbars on inputs/outputs of hepts 
Allowed shrinking hepts main window and added scrollbars on frames
for inputs and outputs.
 2013-10-29 16:48:34 +01:00
Gwenal Delaval
f5872cbcf4 Change URL for sim2chro in manual 
- change URL for download of sim2chro (towards Lustre v4 distribution)
- added GTKWave in INSTALL
- change font of pdf manual
 2013-10-28 12:19:59 +01:00
Gwenaël Delaval
c0b84bd186 Abstraction of integers for Sigali 
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
 2013-09-06 10:13:08 +02:00
Gwenaël Delaval
f3d34f57d1 Abstraction of integers for Sigali 
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
 2013-09-05 19:03:22 +02:00
Gwenal Delaval
17435fd012 Small changes on manual 2013-09-05 14:35:21 +02:00
Gwenal Delaval
6e791e3199 More permissive syntax (trailing commas/semicols) 
Allowing trailing commas and in parameters declarations
 2013-08-02 14:14:14 +02:00
Gwenal Delaval
bb2c3c4060 Update of manual 
- use of GTKWave
- appendix: interfaces of java 1.4 and 1.5 generated code
 2013-08-02 14:14:14 +02:00
Gwenal Delaval
cd01f82cf6 Graphical simulator: output to GTKWave and TikZ 
Added option -gtkwave, output in VCD (Value Change Dump) format

Button for TikZ (tikz-timing) export.
 2013-08-02 14:14:13 +02:00
Gwenal Delaval
ee7ef158e7 Bug correction: java code generation for "~-." 
Bug correction: handling of unary float "~-."
 2013-08-02 14:14:13 +02:00
Gwenaël Delaval
971f622ea3 Added test of camlp4of in configure script 2013-07-18 11:21:27 +02:00
Gwenaël Delaval
71f7db2d11 Bug correction in Mls_printer and Hept_printer 
Correction of infix operators printing : infix printing only
when two arguments of pervasives infix operators (no assertions
on number of arguments).
 2013-07-10 09:57:19 +02:00
Gwenal Delaval
f696203eb1 Bug in sigalimain 
Bug correction: code generation to sigali for stateless nodes

=> stateless nodes handled like stateful nodes, if not in pervasives.
 2013-07-09 21:16:30 +02:00
Gwenal Delaval
2d150a3a3d Infix operators in printers 
Infix operators handled in Heptagon and Minils printers
 2013-07-09 21:15:31 +02:00
Gwenaël Delaval
7720a632cc Removed bugged local substitutions in Contracts pass 2013-05-17 23:21:43 +02:00
Cédric Pasteur
f5cc4625e0 And don't forget to type the argument of when 2013-05-07 17:13:00 +02:00
Cédric Pasteur
21aae319ee Fixed linear typing of when 
It is always a read. One has to use the 
split operator for sampling linear variables.
 2013-05-07 17:09:58 +02:00
Cédric Pasteur
a00620ca19 Fixed interference of fast memories 
A fast memory should be considered alive during
the whole step function when its clock is false.
 2013-05-06 11:47:05 +02:00
Cédric Pasteur
99dc7820c7 Avoid crash in memalloc 
Check if both variables are optmized
 2013-04-22 18:11:10 +02:00
Nicolas Berthier
8497bafa2e Minor but correction in sigali output. 
- Translation to z3z now evaluates constant expressions instead of
  abstracting them. This non-feature could cause "false" synthesis
  failures due to non-translatable yet constant expressions possibly
  introduced by tomato (or manually), for instance `not false' in node
  `n' bellow:

    node n (a: bool) returns (ok: bool)
      contract assume true enforce ok with ()
    let
      ok = a or not false;
    tel
 2013-04-11 17:30:30 +02:00
Nicolas Berthier
899d33afb6 Corrected a bug in generation of C records. 
Corrected a somewhat unnoticeable but ugly bug in the generation of C
records, that could mess up the field names when they were not
assigned in the same order as in the declaration of the type.
 2013-03-15 09:31:19 +01:00
Nicolas Berthier
9db97de879 Bug correction in `Sigalimain.translate_eq'. 
- In Sigalimain: untranslatable non-boolean expressions should not be
  added as inputs of the controller.

- Avoided some compiler warnings in the same module (with OCaml ≥ 4).
 2013-03-12 16:53:52 +01:00
Gwenal Delaval
9b3ba83bb1 Bug correction in java generation 2013-03-11 16:04:12 +01:00
Gwenaël Delaval
f60b00e9e3 Bug correction in Inline_extvalues 
Added handling of controllable variables in Inline_extvalues
 2013-02-08 14:42:26 +01:00
Gwenal Delaval
3a9b332b9b Heptagon manual: pdf version in repository 
(to avoid laborious recompilations)
 2013-02-05 15:33:45 +01:00
Gwenal Delaval
0b5f92b57e Updated configure script 2013-02-05 15:26:49 +01:00
Gwenaël Delaval
5b1784957f Makefile-distrib update 
Makefile-distrib: include install-sh script in source distribution
(mandatory for autoconf).

Enable simulator by default (for automatic builds on pipol: some ctest
versions does not allow options passing to configure scripts).
 2013-02-04 22:16:10 +01:00
Gwenal Delaval
e7f85d6b25 Configuration for binary release 
- custom bytecode compilation
- added suffix (OS, cpu) in binary distrib
 2013-01-28 15:55:56 +01:00
Gwenal Delaval
2be4e287b9 Take into account the -nosink option in Sigali 
Corrected bug: do not suppress the last state
variable when -nosink is on.
 2013-01-28 15:54:27 +01:00
Gwenaël Delaval
165ff8d7fa configure script: SET_MAKE handling 
Change MAKE=@MAKE@ --> @SET_MAKE@
 2013-01-26 13:28:37 +01:00
Gwenaël Delaval
f2c4507ea4 Bug correction in extern_C example 2013-01-25 15:41:34 +01:00
Gwenaël Delaval
dcfcc0f59c Additional Makefiles for distribution builds 
Makefile-bin: only install target, for binary distribution
Makefile-distrib: two targets, binary-distrib (builds a binary distribution
based on the current configuration) and source-distrib (builds a source distribution)
 2013-01-25 00:36:58 +01:00
Gwenaël Delaval
c39a0e058e INSTALL file for distribution 2013-01-24 23:55:35 +01:00
Gwenaël Delaval
5a9b27d6a9 Correct handling of local assume/enforce of contracts 2012-12-11 08:20:04 +01:00
Gwenaël Delaval
d193d3320b Added example "migration" (Bouhadiba et al, Emsoft 2011) 2012-12-11 08:20:04 +01:00
Gwenal Delaval
ce2e2bdcd0 Added -nbvars option for performance evaluation 2012-11-26 10:05:20 +01:00