Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ b8dfc744

# Date Author Comment
b8dfc744 07/12/2019 11:24 PM Pierre-Loïc Garoche

valid _verif node for seal-export lustre

fbcd3ad1 07/12/2019 10:32 PM Pierre-Loïc Garoche

No space in comments

518951ed 07/12/2019 10:24 PM Pierre-Loïc Garoche

Seal export lustre

faf2b835 07/12/2019 10:24 PM Pierre-Loïc Garoche

Work in progress: higher level constructs for lustre elements

5b4c0069 07/12/2019 03:05 AM Pierre-Loïc Garoche

Contract printer cocospec

1561a5bb 07/11/2019 11:25 PM Pierre-Loïc Garoche

No space before contract kwd

096f48d5 07/11/2019 11:23 PM Pierre-Loïc Garoche

Printing trailing zeros in real constants

0292f958 07/11/2019 11:12 PM Pierre-Loïc Garoche

Export cocospec contract

7a4fd94d 07/11/2019 08:59 PM Pierre-Loïc Garoche

Output folder for seal-extract

3fd36dc9 07/11/2019 08:39 PM Pierre-Loïc Garoche

Seal-export to a new file

d75eb6f1 07/11/2019 07:43 AM Pierre-Loïc Garoche

seal-export: produce the output as well. Could be simpler

81229f63 07/11/2019 06:39 AM Pierre-Loïc Garoche

Seal-extract: first serious version. Guards are gathered as a single expression

3b7f916b 07/10/2019 09:16 PM Pierre-Loïc Garoche

Updated version seal-extract

47851ec2 07/09/2019 03:02 AM Pierre-Loïc Garoche

Working version of seal-extract. Heavy load on z3.
TODO: improvement through memoization

7659bbb1 07/09/2019 03:02 AM Pierre-Loïc Garoche

Corelang function: push_negations that propagate negations in leafs of the expression

7aaacbc9 07/07/2019 03:24 AM Pierre-Loïc Garoche

Better extraction in lustrev-seal

58301109 07/07/2019 03:24 AM Pierre-Loïc Garoche

Zustre: Bug solved in const injection for reals

2104c80a 07/06/2019 12:49 AM Pierre-Loïc Garoche

Addressed a TODO in MCDC Pathconditions: simpler condition for single expression

df94cd73 07/06/2019 12:04 AM Pierre-Loïc Garoche

- More systematic translation for mutation
- copy_var_decl now keeps the generated type

e998fc16 07/05/2019 11:15 PM Pierre-Loïc Garoche

Mutation translates now ids in cocospec import

67ef9395 07/04/2019 05:35 PM Pierre-Loïc Garoche

minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.

3050ca8f 07/04/2019 05:34 PM Pierre-Loïc Garoche

keep the open top declaration when loading a module. It may be useful later when producing a lustre file

653b62e0 07/04/2019 05:33 PM Pierre-Loïc Garoche

lustret: do not reload opened modules when generating the mcdc output

8c934ccd 07/04/2019 06:35 AM Pierre-Loïc Garoche

lustrev seal: ongoing work on extraction as dynamical system. Still not working yet

6c3f2837 07/04/2019 06:33 AM Pierre-Loïc Garoche

lustrev: removed the check of no dependencies

49d364b8 07/04/2019 06:32 AM Pierre-Loïc Garoche

comestic changes, removing useless logs

dc6e8512 07/04/2019 01:01 AM Pierre-Loïc Garoche

Merge branch 'ada' into lustrec-seal

e5d77428 05/09/2019 10:19 AM Pierre-Loïc Garoche

Solved issue btw mpfr and conv functions (int_to_real was not handled)

dc732cf2 04/29/2019 10:29 PM Pierre-Loïc Garoche

Solved scopes print order

05f85b44 04/29/2019 01:53 PM Guillaume DAVY

Ada: Start cleaning Ada to prepare for why beckend

c1f565cd 04/19/2019 12:55 PM Guillaume DAVY

Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada

173a2a8f 04/19/2019 12:47 PM Guillaume DAVY

Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second...

325f07c0 04/11/2019 03:16 PM Christophe Garion

doc: use SVG format instead of PNG for dependency graph

aa85bd44 04/11/2019 03:09 PM Guillaume DAVY

Doc: update rule and remove old module in odocl

b5b745fb 04/05/2019 04:37 PM Guillaume DAVY

Ada: First support for transition predicate generation.

867276c9 04/05/2019 04:36 PM Guillaume DAVY

Machine_code: Make a correction in the arrow machine creation :
use the same polymorphic type in variables and values.

2477d634 04/04/2019 04:11 PM Guillaume DAVY

Ada: Correct some errors in printing

230b168e 04/04/2019 02:14 PM Guillaume DAVY

Ada: Refactor Ada Backend to reduce redundancy, make it more modular and
more simple.

2eee868b 03/22/2019 01:51 PM Guillaume DAVY

Merge branch 'lustrec-seal' into ada

826063db 03/22/2019 01:50 PM Guillaume DAVY

Ada: Correct ada main to handle statelles top level node

a4c3d888 03/22/2019 02:05 AM Pierre-Loïc Garoche

rev machines in emf

1f868027 03/22/2019 01:02 AM Pierre-Loïc Garoche

JSON EMF

08788a01 03/21/2019 09:42 PM Pierre-Loïc Garoche

Merge branch 'ada' into lustrec-seal

4034b51c 03/21/2019 09:42 PM Pierre-Loïc Garoche

more explanation in case of failure. Still dirty

f5769e61 03/21/2019 07:55 PM Pierre-Loïc Garoche

Better JSON for EMF backend

861f327f 03/21/2019 07:41 PM Pierre-Loïc Garoche

Resolved sort order of nodes

61e0c3c4 03/21/2019 07:23 PM Guillaume DAVY

Ada:
- Correct the merge with lustrec-seal
- Improve support for builtin function(still work to do)
- Add generation of a gpr file for lib(without main).
- Add var initialisation in the reset, still work to do.

1fd3d002 03/21/2019 05:20 PM Pierre-Loïc Garoche

Cocospec: parsing, normalizing and processing machines for contracts.

42f91c0b 03/21/2019 05:19 PM Pierre-Loïc Garoche

Better EMF output, solved some invalid JSON produced

71999483 03/21/2019 05:18 PM Pierre-Loïc Garoche

Cleaning C backend - removing unused functiions
Preparing for coming ACSL

de671495 03/18/2019 08:31 PM Pierre-Loïc Garoche

Merging branches, disabling the specification print in Ada backend. Should be re-enabled at some point

ab26e196 03/18/2019 04:52 PM Pierre-Loïc Garoche

Merge branch 'lustrec-seal' into ada

d5ec9f63 03/18/2019 04:31 PM Pierre-Loïc Garoche

Minor modif on seal

6517aa0e 03/18/2019 03:34 PM Pierre-Loïc Garoche

Reorganizing folders

c3b0a8c9 03/16/2019 03:28 PM Pierre-Loïc Garoche

Merge branch 'salsa' into lustrec-seal

61df3cb9 03/16/2019 06:23 AM Pierre-Loïc Garoche

Reformating plugin signatures. Better report management

f0a067e9 03/15/2019 10:14 PM Pierre-Loïc Garoche

Better production of trace files.
By default traces are not produced. Requires the option -t to produce them

70be4acf 03/15/2019 12:40 AM Pierre-Loïc Garoche

Serious refactoring of scopes plug-in:
- now properly records the scopes
- only register requested ones

57bf28d9 03/13/2019 05:23 PM Pierre-Loïc Garoche

Merge branch 'unstable' into salsa

6eeafd52 03/13/2019 05:22 PM Pierre-Loïc Garoche

bug solved: issues with main node input access when using scope plugin

525eebd1 03/13/2019 01:27 PM Guillaume DAVY

Ada: Correct branch exporting to handle boolean match(using an ada if)

379715f7 03/13/2019 10:42 AM Guillaume DAVY

Ada: Improve input/output of main ada file

29eebf22 03/12/2019 03:45 PM Pierre-Loïc Garoche

New -salsa-disable option

406818e7 03/12/2019 03:17 PM Pierre-Loïc Garoche

Merge branch 'unstable' into salsa

663e3554 03/12/2019 02:26 PM Pierre-Loïc Garoche

num as a package

6e3cdaf6 03/12/2019 01:18 PM Guillaume DAVY

Ada: Add pretty printer for case

f4cba4b8 03/12/2019 11:23 AM Pierre-Loïc Garoche

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.

8d22ea35 03/12/2019 09:48 AM Guillaume DAVY

Ada: Some indentation

09d7b39f 03/11/2019 07:38 PM Guillaume DAVY

Ada: Add generation of step calls and refactor prototypes and ads printing to handle staless
instance.

3de9f6e4 03/11/2019 02:52 PM Guillaume DAVY

Ada: Refactor the instantiation code and instance code, instead of passing the machine list
to the pp_file and all subfunction in adb generation we pass a list of typed instance which
contains the submachines directly with the instance name and the substitution.

1ed1c8b8 02/26/2019 01:55 PM Guillaume DAVY

Ada: Corrections of some bugs discovered with lustrec-tests

03143434 02/25/2019 01:40 PM Guillaume DAVY

Ada: Add readers and printers for main.adb to match c tests.

2edf6b6d 02/25/2019 01:39 PM Guillaume DAVY

Ada: Add the prefix ada for variable named with an Ada reserved name.

dda9eb32 02/25/2019 01:38 PM Guillaume DAVY

Ada: Correct contract printing

83f4b59c 02/25/2019 01:07 PM Guillaume DAVY

Ada: Correct the subcalls to reset for node with polymorphic type(like arrow)

808da3ff 02/25/2019 12:33 PM Guillaume DAVY

Ada: Correct state print for variable assignement

b1ac8bbf 02/25/2019 11:35 AM Guillaume DAVY

Ada: Add a pp_with for general with ada statement

695db4da 02/25/2019 11:34 AM Guillaume DAVY

Ada: - Replace MStep and Mbranch output by Null to have compilable Ada.
- Correct pp_value to print state access when the variable is memory

721ce555 02/25/2019 10:01 AM Guillaume DAVY

Ada: Removed useless function

ec473179 02/21/2019 10:04 PM Christophe Garion

ada: pretty print assignment statement for state

09b24e7a 02/21/2019 03:49 PM Guillaume DAVY

Ada: Start exporting spec

a2922b84 02/21/2019 03:43 PM Christophe Garion

Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada

c85c2e3d 02/21/2019 03:42 PM Christophe Garion

Ada: pretty printing functions for values and assignments in adb

f2c916b4 02/21/2019 02:27 PM Guillaume DAVY

Ada: Correct some errors on the type checking due to polymorphic type.

8c8d009b 02/21/2019 02:27 PM Guillaume DAVY

Ada: Removed from adb the print of clear and init.

e4b630c5 02/21/2019 02:26 PM Guillaume DAVY

Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into ada

e6492c59 02/21/2019 10:45 AM Guillaume DAVY

Ada: Change some loggging feature

5e54ab9c 02/21/2019 10:01 AM Guillaume DAVY

Ada: Add new function to print package name from node spec to be called by adb backend.

e20d2d2e 02/20/2019 06:23 PM Guillaume DAVY

Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada

9e5f8085 02/20/2019 06:09 PM Guillaume DAVY

Ada: Add support for arrows as an independent generic package, instantiated in each
package using it. It required a lot of refactoring.

f3e8fc18 02/19/2019 11:02 PM Christophe Garion

Ada: typo

08c4ec02 02/19/2019 11:01 PM Christophe Garion

fix conflicts

fd8aeeac 02/19/2019 10:59 PM Christophe Garion

Ada: pretty printing of reset function

903317e7 02/19/2019 05:40 PM Guillaume DAVY

Ada: Remove generation of init and clear and some refactoring around
prototype.

dc429e2f 02/18/2019 02:29 PM Guillaume DAVY

Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada

c203d676 02/18/2019 02:29 PM Guillaume DAVY

Ada Change private to limited private for State type package.

768f60f0 02/14/2019 05:11 PM Christophe Garion

Ada: first pretty printing functions for adb

69cd79c6 02/14/2019 05:02 PM Guillaume DAVY

Ada: Temporary change

4ba20be4 02/14/2019 02:47 PM Guillaume DAVY

Ada: Add local variable declaration for step

2ddbde7d 02/14/2019 02:42 PM Guillaume DAVY

Ada: Last correction was incorrect