Gwenaël Delaval
5a9b27d6a9
Correct handling of local assume/enforce of contracts
2012-12-11 08:20:04 +01:00
Gwenaël Delaval
0e60d2e839
Boolean transformation: added inputs/outputs
...
Non transformation of inputs/outputs during
Boolean pass lead to bugs.
2012-11-22 18:49:12 +01:00
Léonard Gérard
db89208f22
Translate last before removing automatons.
2012-11-05 10:10:32 +01:00
Gwenal Delaval
eddeb1f4de
Bug correction tentative (itfusion)
...
Tentative of correction of itfusion bug:
The itfusion pass adds some "anonymous" nodes into the module.
This correction adds the signature of these created nodes.
This only shifts the bug (towards clocking pass).
2012-09-28 13:06:46 +02:00
Cédric Pasteur
36bfa81b17
Fix for memalloc
...
Take the simplified versions of types (i.e.
with constants instantiated) to check the
equality of types
2012-09-14 16:08:26 +02:00
Cédric Pasteur
96e233b64c
Fix for tuples of consts used as args
2012-09-14 15:42:49 +02:00
Gwenal Delaval
b60ee4b91d
Bug correction in Completion pass
...
Completion pass: do not propagate defnames to
other equations
(see test test_option_flatten_t4 : flatten t4, compile C target code)
2012-08-06 12:04:39 +02:00
Gwenal Delaval
857dccd0b2
Corrected Boolean pass
...
e_level_ck correctly translated
Hept_clocking on stateless functions
2012-08-02 17:24:30 +02:00
Gwenal Delaval
ccab6f7aad
Normalization of record consts
...
Normalization of records as constant to ease the compilation:
f({ x = e })
->
v = { x = e };
f(v)
2012-07-31 16:58:22 +02:00
Gwenaël Delaval
35bea85bf7
Boolean: no transformation on inputs/outputs
...
Only translate local variables, so as to not
modify node interfaces.
2012-07-26 01:45:38 +02:00
Gwenal Delaval
5ed07e1e5a
Removed systematic qual. of infix op as pervasives
...
Bug: every infix operator was systematically qualified
as pervasive.
2012-07-24 17:09:51 +02:00
Cédric Pasteur
84e502d7a9
Made val optional for functions
...
external val node f is a little bit too long
2012-07-04 17:26:38 +02:00
Gwenaël Delaval
ef00823cf7
Added Marc as co-author
2012-06-29 01:43:15 +02:00
Gwenaël Delaval
58086190eb
Headers and license file for GPL
...
Headers for every source file (excluding examples), mentioning
authors, copyright and license (GPL)
COPYING file with GPLv3 content.
2012-06-27 18:14:29 +02:00
Gwenal Delaval
352bad4735
Correction of Inline pass
...
- correction of Hept_mapfold : inclusion of mapfold for b_defnames (blocks)
- Inlining : deep replacement of idents
2012-06-13 15:06:05 +02:00
Gwenal Delaval
cf22ba3989
Optional block in contracts
...
Optional let...tel block in contracts
Sink state in sigali
2012-06-07 17:48:31 +02:00
Gwenal Delaval
2bd31db883
Causality and scheduling with contracts
...
Correction of the causality analysis and scheduling (with interference)
to take contracts into account.
2012-06-07 15:27:07 +02:00
Gwenal Delaval
2956002f85
Correction and simplification of the sigali pass
...
Added a "Contracts" pass, after inlining, taking care of the
contracts of the nodes called in the body of a node. This pass
"inlines" the code and assume/guarantee parts of these subcontracts.
The "Sigali" pass both generates the sigali ("z3z") code and add the call to
the controller (which is a node generated further by the sigali tool).
Therefore this pass has been included into the mls compiler, and removed
from the targets (a "z3z" dummy target has been kept for backward compatibility
reasons).
2012-06-06 15:59:08 +02:00
Gwenal Delaval
bb0bc8bfe5
Added local assume/guarantee
...
Added local assume/guarantee in contracts.
No syntax associated to these local asume/guarantee: internal use only.
2012-05-29 14:14:46 +02:00
Adrien Guatto
6870ea62c9
Inlining: fix issue with nesting of blocks.
2012-03-07 17:48:08 +01:00
Adrien Guatto
3e8e54f42b
Perform inlining before causality/init analysis.
2012-03-07 17:48:08 +01:00
Adrien Guatto
557d00f501
Inlining: do not forget when, merge or last.
2012-03-02 17:12:30 +01:00
Léonard Gérard
8a78bc7d7d
Add [external] in the signatures. fix callgraph acordingly.
2012-02-21 16:07:29 +01:00
Adrien Guatto
070d2eab55
Revert "Changed linear typing for merge."
...
This reverts commit 0abb050a23
.
2012-02-14 14:36:47 +01:00
Adrien Guatto
0abb050a23
Changed linear typing for merge.
...
The new rule accepts that some branches of a linearly typed merge have linear
type Top, provided that at least one has type "lin". E.g.:
node f(x : int at r) returns (o : int at r)
var ck : bool;
let
ck = true;
o = merge ck (x whenot ck) 0;
tel
is now deemed valid.
2012-02-09 16:23:36 +01:00
Adrien Guatto
946a1f8228
Inline extvalues: do not inline array literals.
2012-01-30 16:37:42 +01:00
Adrien Guatto
a7e3f4a973
Added test for clocking in automata
2012-01-25 18:13:43 +01:00
Cédric Pasteur
db5f55b221
Fixed when of stateful exp with memalloc
...
As the expression inside the when will be called
on a faster rhythm, we have to make sure not to
share it with a variable on the slow clock.
We do this by creating a new equation for the
stateful exp.
2012-01-25 09:33:08 +01:00
Léonard Gérard
c75236b688
miscs
2011-12-12 12:06:46 +01:00
Léonard Gérard
da3147151d
Better check signature error message
2011-12-12 11:30:18 +01:00
Léonard Gérard
b86555e013
global env misc
2011-12-12 11:08:47 +01:00
Cédric Pasteur
80fbe6be5f
Fixed linear typing of printf
2011-12-12 10:36:24 +01:00
Cédric Pasteur
54cde301f6
C code generation for printf
2011-12-12 10:36:24 +01:00
Cédric Pasteur
2fc0435393
Added simple printf
...
Typing and clocking done
2011-12-12 10:36:24 +01:00
Léonard Gérard
45fbd18fe8
Fix automaton initialization.
2011-11-28 15:12:27 +01:00
Léonard Gérard
646cfab82b
Enforce style : no tab, no trailing whitespace.
2011-11-21 03:26:27 +01:00
Léonard Gérard
b49c37f7bf
Add ways to declare unsafe functions + unsafe fix
2011-11-21 03:26:26 +01:00
Léonard Gérard
1962cd2df4
Typing bug fix
2011-11-21 03:26:26 +01:00
Léonard Gérard
bdd85f5f81
mapfold over var_ident.
2011-11-18 12:32:36 +01:00
Cédric Pasteur
cf1e79efc8
Type signature of all nodes
2011-11-18 10:03:54 +01:00
Léonard Gérard
0222d11b2d
Do not introduce useless variable in [reset every]
2011-11-03 00:46:13 +01:00
Léonard Gérard
dfc0077859
permits to use = instead of returns
2011-11-03 00:46:04 +01:00
Léonard Gérard
abdf93c8c2
inlining corrected
2011-11-03 00:45:43 +01:00
Léonard Gérard
17598a3206
Correct inlining, which was aliasing clocks.
2011-11-03 00:41:29 +01:00
Léonard Gérard
33021aaa90
Print stateful in heptagon.
...
Conflicts:
compiler/heptagon/hept_printer.ml
2011-11-02 13:15:33 +01:00
Cédric Pasteur
6ba0e7b2b3
Don't remove local variables in causality
...
A dependency between two variables can be caused
by a local variable
2011-10-26 16:14:02 +02:00
Cédric Pasteur
f4aafa10d6
Added a build system for Heptagon
...
./configure
make
make install
2011-10-20 18:06:41 +02:00
Cédric Pasteur
a31715ecde
Proper fix for causality
...
This time it should work in all cases
2011-10-18 09:51:35 +02:00
Cédric Pasteur
85be1252b0
Another try to fix causality of linear ifs
2011-10-17 18:10:38 +02:00
Cédric Pasteur
04b8853a1d
Added a new reinit operator
...
It has type:
reinit: t at r * t -> t at r
It can be used to put a constant value in a
location.
2011-10-17 15:28:04 +02:00