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

973 commits

This branch
This branch
All branches
Author SHA1 Message Date
Gwenal Delaval
41fccc66fb Bugs corrections 
- callgraph: add idents used for instantiated nodes
- cgen : added Idents.enter_node
- cmain : removed error when simulated node does not exist (existence
of simulated node was tested for every program, comprising loaded ones)
 2012-08-01 17:08:58 +02:00
Gwenal Delaval
b858f0e987 Reads and writes of records in main simulation 2012-07-31 16:58:22 +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
ccc07cc7b9 Unalias missing in obc translation 2012-07-31 15:22:38 +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
Gwenaël Delaval
72b1bd8de3 Typo in error message 2012-07-26 01:33:32 +02:00
Gwenaël Delaval
90dda27a3a Bug correction in Schedule_interf 
Bug due to the fact that a variable can be "defined" and "read"
(in scheduling sense) by the same equation, without being a memory:
e.g., a clock defined as the result of a node application, together
with another result on this same clock.

Bug correction: basically removed the "assert false" on killed_vars,
decr_uses; do not count as "use" the self reads.
 2012-07-26 01:29:22 +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
Gwenal Delaval
5890e3599f Light change in test script 2012-07-23 17:36:04 +02:00
Gwenal Delaval
70cb94d0bd Unroll correction 
Order of statement was incorrect
 2012-07-23 17:35:20 +02:00
Gwenal Delaval
6011353cec Added test of options 
Added script test_option which:
- compile and run without option
- compile with option given as argument, run
- diff on the two outputs, fails if different outputs

config file checks for existence of compiler (fails if not exist)

statics1.ept is a copy of statics.ept ; statics2.ept depends on statics1.ept
instead of statics.ept (so as dependency order => lexical order on file names)
 2012-07-19 15:23:40 +02:00
Gwenal Delaval
8b7ad28d6b Some more main in tests 2012-07-18 16:54:44 +02:00
Gwenal Delaval
87f359a6fd Added main to several tests 
Added main to tests
Added dependency statics -> statics2 in scripts
 2012-07-17 17:57:04 +02:00
Gwenal Delaval
891b1f3ffd Added some main in tests 
Goal: run as many nodes as possible
 2012-07-16 18:49:08 +02:00
Gwenal Delaval
40cf503149 Correct test scripts config file 
Added "mkdir _check_builds" if it does not exist
 2012-07-16 18:48:03 +02:00
Gwenal Delaval
295997b866 Config of test scripts 
Added option -stdlib towards source library
 2012-07-16 16:16:59 +02:00
Gwenal Delaval
9c51b91fd3 Correct ctest configuration 
SET_TEST_PROPERTIES does not work with ctest < 2.8.0
 2012-07-16 16:12:16 +02:00
Gwenal Delaval
7e90dccc0a Cleared java simulation output 2012-07-16 11:37:50 +02:00
Gwenal Delaval
4c0b1f8431 Corrected ctest configuration file 2012-07-16 11:22:56 +02:00
Gwenal Delaval
89ee2a8fb6 Manual: part on automata 
Paragraphs about type of transitions
weak/strong, memoryles/with memory
 2012-07-16 09:54:12 +02:00
Gwenaël Delaval
e424667f47 Tests with ctest 
Configuration files and scripts to perform tests with ctest
- ctest can be run into the test directory or the root
- the script CTestScript.cmake allows ctest to perform the whole
sequence update/configure/build/test and submit the result to
cdash (http://cdash.inria.fr/CDash/index.php?project=Heptagon)
- gen_ctests is used to generate the file test/CTestTestfile.cmake
 2012-07-16 01:03:37 +02:00
Gwenaël Delaval
90e391f4df Modified test t13.ept 
Modified test t13.ept so that the output is not always "0"
(useful for further comparisons)
 2012-07-16 01:00:09 +02:00
Gwenaël Delaval
a15e17c02d Cleared simulation output 2012-07-16 00:58:40 +02:00
Gwenaël Delaval
bcfcf8cf39 Added iostream in standard library 2012-07-14 14:35:34 +02:00
Gwenaël Delaval
e103d60c26 Removed eprintf in schedule_interf 
eprintf -> Interference.print_debug
 2012-07-14 14:31:46 +02:00
Gwenal Delaval
2e0abee73c Added web site 
First version of web site

URL of on-line web site is http://heptagon.gforge.inria.fr

The script rsyncweb allows to sync between the repository and the online site (by use of rsync)
 2012-07-12 16:08:36 +02:00
Gwenal Delaval
11493f3274 Manual 
UpDown automaton (figure)

Changes in the structure: contracts within Section "Syntax and informal semantics"
 2012-07-05 17:26:29 +02:00
Gwenal Delaval
bea0c5ac7c Manual: section on compilation and install 
Manual: section on compilation, install, required tools and libraries
 2012-07-05 16:14:39 +02:00
Cédric Pasteur
09202bd9ec Remove graphical syntax 2012-07-05 11:59:16 +02:00
Cédric Pasteur
767883d578 Small fixes 2012-07-05 11:46:30 +02:00
Cédric Pasteur
9e17900f13 Small section on linear annotations 2012-07-05 11:19:43 +02:00
Cédric Pasteur
a2b694602f Small section on clocks 2012-07-05 10:14:04 +02:00
Cédric Pasteur
03acfc9bea New sections in the manual 
arrays, records, parametricity, etc.
 2012-07-05 08:51:46 +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
a0e0bd2dcc Radio transmitter example 
Radio transmitter example, from Nicolas Berthier's thesis

With controller synthesis

Generic Makefile including controller synthesis handling
 2012-06-29 02:28:42 +02:00
Gwenaël Delaval
bf03077cd9 Correct output toward hepts 2012-06-29 02:01:49 +02:00
Gwenaël Delaval
ef00823cf7 Added Marc as co-author 2012-06-29 01:43:15 +02:00
Gwenaël Delaval
c080ad6cf3 Controller call only when controllables 
Avoid built of dummy empty controllers
 2012-06-29 01:41:13 +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
Cédric Pasteur
5e1dad630b Force fby to be scheduled at the end 2012-06-20 17:09:30 +02:00
Cédric Pasteur
7a10ba028a Fixed disjoint clock computation 2012-06-20 17:09:17 +02:00
Cédric Pasteur
ffeb81f529 Use idents instead of ivars in scheduling 2012-06-20 16:33:06 +02:00
Cédric Pasteur
8815a2cd03 Better handling of clocks in memalloc 
- We can do a better allocation if we take into
account 'when' in extvalues 
(test/good/memalloc_clocks.ept shows the
improvement)
- Fixed a bug with memalloc on records: if we 
translate:
o = { a with .f = u }
to
o = a; o.f = u
then we cannot share u and o.f
 2012-06-20 09:17:13 +02:00
Cédric Pasteur
ee7d60120b Fixed bug in translation to minils 2012-06-19 15:56:54 +02:00
Cédric Pasteur
ed2c08315b Should be affinity, not copy 2012-06-19 09:33:27 +02:00
Gwenal Delaval
d36e988fb9 User manual: first version 2012-06-14 23:07:40 +02:00
Gwenal Delaval
502c5e446f Makefile correction (install target) 
Makefile correction: install target for simulator
 2012-06-13 15:13:53 +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