Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ 587cdc0d

History | View | Annotate | Download (14.6 KB)

# Date Author Comment
587cdc0d 06/25/2014 05:00 PM Pierre-Loïc Garoche

Solved Bug in horn backend: when main node is stateless

7130028e 06/25/2014 07:45 AM Pierre-Loïc Garoche

Solved local var name bugs for stateless nodes as outlined by Teme

aa223e69 03/10/2014 09:55 AM Xavier Thirioux

more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--

M trunk/src/corelang.mli
M trunk/src/type_predef.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M trunk/src/typing.ml...

9334747d 02/24/2014 04:26 PM Pierre-Loïc Garoche

Fixed bug on the main part

3e209698 02/24/2014 11:47 AM Pierre-Loïc Garoche

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

3a60ec17 02/24/2014 11:25 AM Pierre-Loïc Garoche

...

4f3cc9f3 02/24/2014 10:50 AM Pierre-Loïc Garoche

Is it working?

c0003810 02/24/2014 09:46 AM Pierre-Loïc Garoche

Working on bugs

40f8d0f9 02/21/2014 05:11 PM Pierre-Loïc Garoche

Second (almost) working version

faa5e5c5 02/21/2014 04:39 PM Pierre-Loïc Garoche

First (almost) working version

fc7a01ce 02/21/2014 12:42 PM Pierre-Loïc Garoche

Ongoing ...

23bdf881 02/21/2014 12:38 PM Pierre-Loïc Garoche

Ongoing ...

04a7df69 02/21/2014 08:37 AM Pierre-Loïc Garoche

In the middle of the coding process. Just pushing thinks

aa6b7d46 02/20/2014 06:45 AM Pierre-Loïc Garoche

The missing file