Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec-tests
seal target
Seal targets
Added function pure real
add lm challenges
array example with spec
Clock issue
add simpler triplex example
New folder for extraction testing
add ada_diff.py
Renamed main node as top
Missing dep for ADA targets
Solving issue in the ADA test cases
rapport de stage modèle word
base3_correct intégré et simulé ous vivado
Added some vhdl examples for vhdl->lustre translation and a first proposition of encoding
Premier exemple de code VHDL
add case where emf order is not good
add examples with clock
Updated scripts (emf->json)
Top level contracts are comments
Removed mode labels
Small modifications to have the tests ok: we do not handle yet the ::mode_id syntax
Moved files content in a single file
add regulators cocospec example
Merge branch 'guarantees'
Merge branch 'master' into guarantees
guarantee(s)
remove corrupted lustre files
add ADA strategy and call it in Simulink folder
cleanup src_many_files, regenerate input/output references
No temporary file on repo!
add more cocospec examples
add another contract example
Added JSON files for valencia VHDL tests
Major update of vhdl tests
Update of vhdl samples files
Samples cleaning
add more simulink tests
add include test
update zustre reference
Updated ref output
Better naming
add output references
renamed mode as mode_ to avoid collision with the mode keyword of cocospec.
Script now compare the output with ones compiled with the same options
Moved to cocospec contract
Restructured mpfr folder tests to rely on highlevel strategies
Improved the diff tests: a new option allow to use the java test parameterized by epsilon (precision). Default bnehavior is using regular diff on files
Renamed math in lustrec_math
Improved ctest configuration
Update of makefile
Update of test cases with new version of Linty VHDL parser
Added makefile to launch tests
Scheduling issue
Renaminig lustre contracts from ensures to guaranteesWill require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)
Cocospec
add more contracts examples
Correct version of the two_counters exported json file
Cocospec files
Added two_counters example
Counters, programmable pulse, d-latch VHDL examples
Improving integration with CDash
Update of d-latch sample
Added test laucher for lustre generation
Continue even if generation fails
Makefile update for new version of lustrei with command line parameters
Test file update for typo
Added example from some courses
Updated tests for lustrei vhdl import
Added tests for vhdl import and export (pp)
Tiny example for zustre debugging
add Kind2Results
Updates some expected outputs
add zustre results
add json regression tests
add helpful_functions to the modules folder
stopwatch
Simple test to show cex with zustre
More functions
More tests
New machine types related test cases
add new format
add json example for SF IR
MPFR and EMF checks