Project

General

Profile

Activity

From 03/05/2019 to 04/03/2019

04/03/2019

04:00 AM Bug #76 (New): Import error: Load error: imported node real_to_int declared in a regular Lustre ...
*Branch used: Seal version 1.7-1000-lustrec-seal (Xia/Huai-dev)*
*lustrec -horn -d toto -algebraic-loop-solve ap_12B...
Hamza Bourbouh
03:58 AM Bug #75 (New): exception File "checks/algebraicLoop.ml", line 368, characters 16-22: Assertion fa...
*Branch used: unstable (up to date)*
*lustrec -I /Users/hbourbou/Documents/cavale/local/include/lustrec -horn -d tot...
Hamza Bourbouh

03/30/2019

03:34 AM Bug #74 (New): const is not supported inside contract
When defining constants inside contract, their definition is ignored in json output, but their call is not impacted.
...
Hamza Bourbouh

03/28/2019

08:19 PM Bug #73 (New): properties ID is not set in Json in EMF backend
guarantee "propertyID" P;
propertyID is missing in the generated json.
An example is attached.
Hamza Bourbouh

03/22/2019

01:51 PM Revision 2eee868b (lustrec): Merge branch 'lustrec-seal' into ada
Guillaume DAVY
01:50 PM Revision 826063db (lustrec): Ada: Correct ada main to handle statelles top level node
Guillaume DAVY
03:56 AM Bug #72 (New): Simulinkd does not match Lustre using EMF backend when using nested Merge expression
Lustre attached uses merge and one of merge branches is a call to another node with a merge inside.
Inside merge, th...
Hamza Bourbouh
02:16 AM Revision 9fb1ab37 (lustrec): Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustre...
Garoche
02:15 AM Revision 75a7b65b (lustrec): install notes
Garoche
02:05 AM Revision a4c3d888 (lustrec): rev machines in emf
Pierre-Loïc Garoche
01:46 AM Lustrec-Tests Revision e45f370e (lustrec-tests): add case where emf order is not good
hbourbou
01:40 AM Lustrec-Tests Revision 160ddb22 (lustrec-tests): Merge branch 'master' of https://cavale.enseeiht.fr/git/lustre...
hbourbou
01:39 AM Lustrec-Tests Revision b58cc410 (lustrec-tests): add examples with clock
hbourbou
01:02 AM Revision 1f868027 (lustrec): JSON EMF
Pierre-Loïc Garoche

03/21/2019

12:45 AM Lustrec-Tests Revision 9ca1404d (lustrec-tests): Updated scripts (emf->json)
Pierre-Loïc Garoche
09:42 PM Revision 08788a01 (lustrec): Merge branch 'ada' into lustrec-seal
Pierre-Loïc Garoche
09:42 PM Revision 4034b51c (lustrec): more explanation in case of failure. Still dirty
Pierre-Loïc Garoche
09:41 PM Lustrec-Tests Revision ffe46d5f (lustrec-tests): Top level contracts are comments
Pierre-Loïc Garoche
09:38 PM Lustrec-Tests Revision 3debaf88 (lustrec-tests): Removed mode labels
Pierre-Loïc Garoche
09:29 PM Lustrec-Tests Revision 2a9aa5e1 (lustrec-tests): Merge branch 'master' of https://cavale.enseeiht.fr/git/lustre...
Pierre-Loïc Garoche
09:29 PM Lustrec-Tests Revision 4784e95f (lustrec-tests): Small modifications to have the tests ok: we do not handle yet...
Pierre-Loïc Garoche
09:28 PM Lustrec-Tests Revision f0e4e301 (lustrec-tests): Moved files content in a single file
Pierre-Loïc Garoche
08:25 PM Lustrec-Tests Revision 6ccfcb12 (lustrec-tests): add regulators cocospec example
hbourbou
07:55 PM Revision f5769e61 (lustrec): Better JSON for EMF backend
Pierre-Loïc Garoche
07:41 PM Revision 861f327f (lustrec): Resolved sort order of nodes
Pierre-Loïc Garoche
07:23 PM Revision 61e0c3c4 (lustrec): Ada:
- Correct the merge with lustrec-seal
- Improve support for builtin function(still work to do)
- Add generation o...
Guillaume DAVY
05:20 PM Revision 1fd3d002 (lustrec): Cocospec: parsing, normalizing and processing machines for contracts.
Pierre-Loïc Garoche
05:19 PM Revision 42f91c0b (lustrec): Better EMF output, solved some invalid JSON produced
Pierre-Loïc Garoche
05:18 PM Revision 71999483 (lustrec): Cleaning C backend - removing unused functiions
Preparing for coming ACSL Pierre-Loïc Garoche
05:16 PM Lustrec-Tests Revision b8c35852 (lustrec-tests): Merge branch 'guarantees'
Pierre-Loïc Garoche
05:15 PM Lustrec-Tests Revision 61a7e719 (lustrec-tests): Merge branch 'master' of https://cavale.enseeiht.fr/git/lustre...
Pierre-Loïc Garoche
05:15 PM Lustrec-Tests Revision 85dbaa74 (lustrec-tests): Merge branch 'master' into guarantees
Pierre-Loïc Garoche
05:12 PM Lustrec-Tests Revision bd3f748f (lustrec-tests): guarantee(s)
Pierre-Loïc Garoche

03/20/2019

12:32 AM Lustrec-Tests Revision 99a9d521 (lustrec-tests): remove corrupted lustre files
hbourbou
02:48 AM Lustrec-Tests Revision 17b2e00a (lustrec-tests): add ADA strategy and call it in Simulink folder
hbourbou

03/19/2019

03:21 AM Lustrec-Tests Revision 36b093bd (lustrec-tests): cleanup src_many_files, regenerate input/output references
hbourbou

03/18/2019

10:29 PM Revision 4d2d6777 (lustrec): INSTALL file
Pierre-Loïc Garoche
08:31 PM Revision de671495 (lustrec): Merging branches, disabling the specification print in Ada backend. ...
Pierre-Loïc Garoche
04:52 PM Revision ab26e196 (lustrec): Merge branch 'lustrec-seal' into ada
Pierre-Loïc Garoche
04:31 PM Revision d5ec9f63 (lustrec): Minor modif on seal
Pierre-Loïc Garoche
03:34 PM Revision 6517aa0e (lustrec): Reorganizing folders
Pierre-Loïc Garoche

03/16/2019

04:00 PM Lustrec-Tests Revision cd1faebc (lustrec-tests): No temporary file on repo!
Pierre-Loïc Garoche
03:28 PM Revision c3b0a8c9 (lustrec): Merge branch 'salsa' into lustrec-seal
Pierre-Loïc Garoche
06:23 AM Revision 61df3cb9 (lustrec): Reformating plugin signatures. Better report management
Pierre-Loïc Garoche

03/15/2019

10:14 PM Revision f0a067e9 (lustrec): Better production of trace files.
By default traces are not produced. Requires the option -t to produce them Pierre-Loïc Garoche

03/14/2019

12:40 AM Revision 70be4acf (lustrec): Serious refactoring of scopes plug-in:
- now properly records the scopes
- only register requested ones
Pierre-Loïc Garoche
08:27 PM Lustrec-Tests Revision f470cec6 (lustrec-tests): add more cocospec examples
hbourbou

03/13/2019

05:23 PM Revision 57bf28d9 (lustrec): Merge branch 'unstable' into salsa
Pierre-Loïc Garoche
05:22 PM Revision 6eeafd52 (lustrec): bug solved: issues with main node input access when using scope plugin
Pierre-Loïc Garoche
01:27 PM Revision 525eebd1 (lustrec): Ada: Correct branch exporting to handle boolean match(using an ada if)
Guillaume DAVY
10:42 AM Revision 379715f7 (lustrec): Ada: Improve input/output of main ada file
Guillaume DAVY

03/12/2019

03:45 PM Revision 29eebf22 (lustrec): New -salsa-disable option
Pierre-Loïc Garoche
03:17 PM Revision 406818e7 (lustrec): Merge branch 'unstable' into salsa
Pierre-Loïc Garoche
02:26 PM Revision 663e3554 (lustrec): num as a package
Pierre-Loïc Garoche
01:18 PM Revision 6e3cdaf6 (lustrec): Ada: Add pretty printer for case
Guillaume DAVY
11:23 AM Revision f4cba4b8 (lustrec): Some progress on compiling cocospec contract.
Contract resolution still need to be done as well as dealing with the machine code level and so on. Pierre-Loïc Garoche
09:48 AM Revision 8d22ea35 (lustrec): Ada: Some indentation
Guillaume DAVY

03/11/2019

09:58 PM Bug #69 (Closed): fatal error: bracket nesting level exceeded maximum of 256
I solved the issuer by adding "-fbracket-depth=10000" to GCC option while running make. Hamza Bourbouh
09:55 PM Bug #71 (Closed): C code generation failed
lustrec -node ForIterator_bio_bug_PP ForIterator_bio_bug_PP.LUSTREC.lus
make -f ForIterator_bio_bug_PP.LUSTREC.makef...
Hamza Bourbouh
07:38 PM Revision 09d7b39f (lustrec): Ada: Add generation of step calls and refactor prototypes and ads pr...
instance. Guillaume DAVY
02:52 PM Revision 3de9f6e4 (lustrec): Ada: Refactor the instantiation code and instance code, instead of p...
to the pp_file and all subfunction in adb generation we pass a list of typed instance which
contains the submachines ...
Guillaume DAVY
 

Also available in: Atom