Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ 19a1e66b

History | View | Annotate | Download (26.5 KB)

# Date Author Comment
59803095 11/16/2018 11:30 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal
c35de73b 11/15/2018 03:18 AM Pierre-Loïc Garoche

Pretty serious update:
- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue):
when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....
b0c381d0 07/12/2018 04:04 PM Pierre-Loïc Garoche

Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
1d0fd52b 05/18/2018 12:28 AM Xavier Thirioux

updated division for Horn clauses
2bb5ab71 05/17/2018 04:57 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal
fa91d4d0 05/17/2018 03:14 PM Pierre-Loïc Garoche

Euclidean div/mod treatment in Horn backend
e4edf171 04/03/2018 04:38 PM Pierre-Loïc Garoche

Zustre backend
ea8f51ae 03/30/2018 11:23 PM Pierre-Loïc Garoche

Basic library printers moved into backend specific printer files
2863281f 03/30/2018 11:14 PM Pierre-Loïc Garoche

Further restructuring:
- arrow.ml* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines
8446bf03 03/30/2018 05:54 PM Pierre-Loïc Garoche

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types
66359a5e 01/31/2018 07:27 AM Pierre-Loïc Garoche

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program
212d6eff 07/13/2017 06:40 PM Pierre-Loïc Garoche

[HORN] handled asserts in stateless node step rule definition
07ceae4c 07/13/2017 05:47 PM Pierre-Loïc Garoche

[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github: https://github.com/coco-team/lustrec/issues/13
397d5ae3 06/27/2017 06:36 PM Pierre-Loïc Garoche

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output
3ca27bc7 06/23/2017 04:07 AM Pierre-Loïc Garoche

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information
a6974c82 05/17/2017 12:21 PM Pierre-Loïc Garoche

[Horn] Workaround to prevent the use of declared keywords as node name
2fdbc781 04/27/2017 10:42 PM Pierre-Loïc Garoche

Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed
dcafc99b 01/11/2017 12:28 AM Pierre-Loïc Garoche

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al
44ce4da8 01/04/2017 12:30 AM Pierre-Loïc Garoche

Solved some issues with commited code (like it doesn't compile). The code was written by Teme's student and
- did not rely on existing typing.ml function
- used strange fprintf code

Code was refactored but old stuff kept in comment just in case. Will have to be cleaned at some point.
e057dd08 12/30/2016 10:47 PM Teme Kahsai

adjusting travis
7ad4ff7c 12/30/2016 09:29 PM Teme Kahsai

Merge branch 'master' into master
1b57e111 12/30/2016 09:20 PM Teme Kahsai

adding sfunction support
822f31e1 12/08/2016 05:55 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04
84902260 10/12/2016 11:44 PM jbraine

Arrays
85a6f473 09/30/2016 06:41 PM Teme Kahsai

adding onera automata version
f3d244c1 08/09/2016 10:01 PM Xavier Thirioux

...
45f0f48d 08/09/2016 09:31 PM Xavier Thirioux

...
fea041c5 08/09/2016 09:25 PM Xavier Thirioux

new branch for merging mpfr and horn