CristalCaveGem » LustreC

Working example!

Pom pom pom

Sample value for VHDL

Compiling - while doing nothing :)

Bootstrapping VHDL importer/exporter

updated division for Horn clauses

corrected euclidean division in C code

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

introduced euclidean/C-like division in C code generation

Euclidean div/mod treatment in Horn backend

Issues with typing pp_basic_lib_fun

Tuning the pretty printing of Salsa plugin

Basic library printers moved into backend specific printer files

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

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

Recursive resolution of dependencies

[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

Type issue Bytes vs string

[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.

[EMF] Less verbose

[EMF] adding original name field in the JSON

[EMF] Added the reset signal (the every argument) as input to the JSON struct

Solving a warning with ocaml 4.04 and uppercase_ascii. Provides backward compatibility for 4.02

Issue with clocked expressions. Now handled throught a local branch, ie. a single action block in Simulink

C backend: solved the issue of long name in generated binaries.

first solution to address very large identifiers in node names, logs, and generated binaries

[EMF] improved feedback on reset calls

Merge branch 'dynamic_inlining' into unstable

[EMF} missing brace

[EMF] missing quotes

Merge branch 'unstable' into dynamic_inlining

[EMF] improved alignement of braces + solved (naother) bug in shortening of ids

[EMF] more hash

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

[EMF] bug solved, some ids were not hashed

ange ID length

blup

[EMF] simplify branches with single case as regular instructions

[EMF] Disable join of guards in EMF backend

Refactor error printing.

[EMF] protect machine names

[EMF] protect more field

[EMF] Protecting print of names to ensure a length < 50. Remove the middle part of the string and inject a hash of it.

Renamed math lib into lustrec_math to avoid conflicting calls to <math.h>

[HORN] handled asserts in stateless node step rule definition

[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

Provides type compatible with Matlab types in EMF backend

[EMF backend] Merging branches

Refactored some code: optimization of machine

bug fixed: Inputs for branches solved

Proper integer index for enumerated branches

Enumerated datatypes as integer

Refactored EMF backend. Handle now the call to existing math and conv libraries

EMF backend: each branch provides the inputs and outputs

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

small modifs in EMF format

Branchs output in EMF is only the intersection of each branch defined flows

Full rewrite of EMF backend.

Ongoin work on EMF backend. Commit to store a working version. More work to do on clocks and resets

Improved EMF backend. Working on the whole fmcad suite

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

- Added a field lustre_eq to machine instruction in order to record the originating lustre equation
- EMF backend now impose the optimization level to be set to 0 in order to avoid equation elimination that would render traceability difficult
- Options.ml has been split into Options.ml / Options_management.ml. Options.ml only contains references and no functions

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information

- Added a precision parameter for io_frontend "real" types
- New fonction in plugins: main_loop_body_prefix

Changed encoding of matlab expression inputs from u(xx) to uxx.

EMF backend now relies on machine code representation.
Impact:
- EMF backend has an extra machines argument
- specific option to avoid merge of ite constructs
- set_backend function to improve backend selection

Most code was extracted from seahorn_backend through c0f8

fixed matlab output

Changed the matlab function backend

Missing file

fixed matlab output

Changed the matlab function backend

Merge branch 'unstable' into seahorn_a6df3
a6df3 is the initial commit of branch seahorn

[Horn] Workaround to prevent the use of declared keywords as node name

Solved printing bug in Horn backend

Improved include folders behaviors:
- allow multiple -I dir, will be used in order (first one declared
is first used)

- when declaring a global library #open <foo>, foo is first checked
in local folders, than in global one (install path). This
does not apply to local libraries opened with #open "foo".

trying to improving pretty printing. Not so perfect for the moment

Missing file c_backend_lusic

Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed

Merge branch 'unstable' into merge_mauve_unstable

Merge branch 'testgen' into merging_unstable_testgen

Missing files

Merge branch 'unstable' into merging_plugins
Non regression results were similar to master branch

Printing reals in Horn backend

Cosmetic changes

More informative error message in case of untyped value

Deprecated function changed for compatibility with ocaml 4.04

This is the first merge that does compile. Not tested yet.

adding dealloc

Merge branch 'master' into mauve

added deallocation for dynamic memory allocation scheme

adding & in shell

mauve generator with annotations

mauve generator: first shot

adding c++ backend

fix tracebility

Working on EMF backend to express cocospec infos as Simulink blocks

[Horn] Updated traceability of Horn backend to deal with fby (arrow machines)

Revert some ocaml code to ocaml 4.01 compatibility

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al