Project

General

Profile

Activity

From 05/02/2018 to 05/31/2018

05/31/2018

04:39 PM Revision 0bd19a92 (lustrec): bug wrt normalization. Didn't take clock into account.
Xavier Thirioux
04:35 PM Revision bec3cf3d (lustrec): strange bug (ill-typed source) wrt Bytes/String conversion
Xavier Thirioux
04:33 PM Revision cff64531 (lustrec): bug in CSE, was disregarding clock
Xavier Thirioux
02:59 PM Revision 885b2896 (lustrec): Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
Xavier Thirioux
01:47 PM Revision 22a34b49 (lustrec): json-parser: starting changing datatypes
Christophe Garion
11:33 AM Bug #66 (Closed): Lustrec generates different outputs for the same code
Attached is 2 Lustre files, they have common code defining the first output of the main node.
The binary of both Lus...
Hamza Bourbouh

05/30/2018

04:02 PM Revision 2f7c9195 (lustrec): zustre progress. Issues with sliced predicates
Pierre-Loïc Garoche
11:49 AM Lustrec-Tests Revision fd5381b7 (lustrec-tests): stopwatch
Bourbouh

05/29/2018

08:59 PM Revision 3d3718ae (lustrec): package z3 to Z3 when using z3 github repo.
Pierre-Loïc Garoche
01:49 PM Revision df00d682 (lustrec): Adding input in MAIN fdecl
Pierre-Loïc Garoche
09:56 AM Lustrec-Tests Revision 75bb7d62 (lustrec-tests): Simple test to show cex with zustre
Pierre-Loïc Garoche
12:10 AM Revision 5275a6fd (lustrec): [lustrev] forced the z3 lib to be loaded before others when using the provided bash script.
Pierre-Loïc Garoche
12:09 AM Revision dbab1fe5 (lustrec): [lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result
Pierre-Loïc Garoche

05/20/2018

11:45 PM Revision 9a9058f4 (lustrec): More work on Salsa plugin
Pierre-Loïc Garoche

05/18/2018

04:08 PM Revision 4c8a5ae4 (lustrec): [salsa] more debug messages
Pierre-Loïc Garoche
04:02 PM Revision bc504848 (lustrec): corrected kind parsing
Xavier Thirioux
02:22 PM Revision 9b348db1 (lustrec): [salsa] introducing sliced temporal variables
Pierre-Loïc Garoche
08:05 AM Revision 9f3de818 (lustrec): Some progress on zustre
Pierre-Loïc Garoche
12:28 AM Revision 1d0fd52b (lustrec): updated division for Horn clauses
Xavier Thirioux

05/17/2018

05:08 PM Revision 14da5302 (lustrec): corrected euclidean division in C code
Xavier Thirioux
05:04 PM Revision 58d610e1 (lustrec): corrected the division conversion scheme
Xavier Thirioux
04:59 PM Revision 8cc55e2c (lustrec): corrected the division conversion scheme
Xavier Thirioux
04:57 PM Revision 2bb5ab71 (lustrec): Merge branch 'unstable' into lustrec-seal
Pierre-Loïc Garoche
03:50 PM Revision a6e85cdc (lustrec): Integer div choices
Pierre-Loïc Garoche
03:49 PM Revision eccb3f63 (lustrec): Provide back the previous behavior concerning parsing spec.
Pierre-Loïc Garoche
03:45 PM Revision 4d7f8ce0 (lustrec): Merge branch 'cocospec' of https://cavale.enseeiht.fr/git/lustrec into unstable
Pierre-Loïc Garoche
03:32 PM Revision ba91ed9e (lustrec): Merge branch 'euclidean' into unstable
Pierre-Loïc Garoche
03:32 PM Revision 0e1a5ece (lustrec): Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
Pierre-Loïc Garoche
03:31 PM Revision 91f0f06a (lustrec): Merge branch 'euclidean' of https://cavale.enseeiht.fr/git/lustrec into euclidean
Pierre-Loïc Garoche
03:29 PM Revision 5318ad88 (lustrec): introduced euclidean/C-like division in C code generation
Xavier Thirioux
03:15 PM Revision c2db548b (lustrec): install of yojson depends on lustresf in configure now
Christophe Garion
03:14 PM Revision fa91d4d0 (lustrec): Euclidean div/mod treatment in Horn backend
Pierre-Loïc Garoche
02:42 PM Revision 3cd040e3 (lustrec): Issues with typing pp_basic_lib_fun
Pierre-Loïc Garoche

05/16/2018

05:19 PM Revision 12249005 (lustrec): Kind licence file
Pierre-Loïc Garoche
05:19 PM Revision 2ae3ef3f (lustrec): Tentative to rely on Kind parser for contracts
Pierre-Loïc Garoche
04:33 PM Bug #58 (Closed): int to long long int
Already supported by option -real or -int Pierre-Loïc Garoche
04:32 PM Bug #64 (Closed): Typing error
Pierre-Loïc Garoche
04:31 PM Bug #64 (Resolved): Typing error
Not a typing error in secret unstable branch Pierre-Loïc Garoche
04:30 PM Bug #65: integer division (euclidein division)
Considering producing valid integer division and modulo instead of C ones. To be discussed. Pierre-Loïc Garoche
03:34 PM Revision ff6ba54e (lustrec): Produce condition coverage for basic boolean expressions. To be improved with a simpler condition.
Pierre-Loïc Garoche

05/15/2018

02:38 PM Revision 8cacf677 (lustrec): [lustrec/mcdc/ improved the MCDC output
Pierre-Loïc Garoche
11:49 AM Revision 8e6cab20 (lustrec): Tuning the pretty printing of Salsa plugin
Pierre-Loïc Garoche

05/08/2018

10:39 PM Bug #65 (Closed): integer division (euclidein division)
node top(x, y:int)
returns(z:int);
let
z = x/y;
tel
This is translated as x/y in C, which is different fro...
Hamza Bourbouh

05/07/2018

03:20 PM Revision 151117f7 (lustrec): Homogenizing the API for salsa and its use within the plugin
Pierre-Loïc Garoche

05/04/2018

08:01 PM Revision 68322df3 (lustrec): Some tentative improvement of Salsa plugin. Not satisfying yet
Pierre-Loïc Garoche
08:00 PM Revision 7065d912 (lustrec): Moved mk_fresh_var from normalization to corelang
Pierre-Loïc Garoche
05:42 PM Revision 8926852f (lustrec): [scopes] Producing the appropriate scope label
Pierre-Loïc Garoche
05:09 PM Revision 08faae63 (lustrec): NumMartel functions
Pierre-Loïc Garoche

05/03/2018

08:35 AM Revision b068041a (lustrec): Merging unstable into salsa
Pierre-Loïc Garoche
08:35 AM Revision c0d116ec (lustrec): Merge branch 'unstable' into salsa
Pierre-Loïc Garoche
 

Also available in: Atom