BDDC is a basic logical calculator.
Distribution (binaries) User manual Printable (pdf)
Reglo compile regular expressions into logical circuits (in Lustre).
Distribution (binaries) User manual Printable (pdf)
Introduction yacc2latex translates a yacc or ocamlyacc (mly) file into an hopefully pretty EBNF grammar, and then in Latex.
For language developers, it’s rather tedious and error-prone to write and maintain a reference (printable and readable) grammar of their language. Indeed, the “actual” grammar independent from the “actual” one, often written in yacc or mlyacc.
yacc2latex allows to “compile” a yacc/mly source into a latex file that can be easily integrated into the reference manual of the language (supposing that latex is used for document processing).
Yacc2latex generates human-readable EBNF grammars from yacc files. Output format is in Latex and fairly customizable.
Distribution yacc2latex is available under LGLP licence
Dowload
How to install
Short Manual
Goal As a language designer, I often faced the problem of writing and maintaining a reference (readable) grammar of my language. This is particularly annoying since the reference grammar actually exists as a yacc (or ocamlyacc) file, so why not use a “compiler” that will derived automaticaly the reference grammar from the yacc file ?
Short Manual Version: 3.0-r4dcb390 Pascal Raymond (Home Page) Usage yacc2latex version 3.0-r4dcb390 usage: yacc2latex <option> | yacc2latex -help -m : print a short manual -md : same in markdow format -t <file>: load token def file -o <file>: set out file (default infile.tex) -os : write output to stdout -- : read input from stdin -main : gen a sample main latex file) -testl : dump the yacc tokens and stop -testy : dump the yacc grammar and stop -testg : dump the ebnf grammar and stop -version : print version and stop -v : set verbose mode -dbg {main}: set debug flag -help Display this list of options --help Display this list of options Tokens file Must contain one token definition per line:
tagada – Task dAg GenerAtor Doubtful Acronym This tool generates random task graphs (precisely, Direct Acyclic Graphs, DAG). The Typical usage is to provide test cases for mapping and scheduling algorithms.
Installation The distribution is avalaible on Gricad-Gitlab.
From sources Compiling requires an opam based OCaml environment. Recommanded opam version: 2.1. Recommanded OCaml switch (version) >= 4.14 Mandatory packages:
dune >= 3.0 yaml >= 3.0 Binary A Linux-x86_64 binary is provided in the distribution.
This Toolbox gathers currently maiontainde tool around Lustre and the synchronous approach, in particular the The Lustre V6 compler and the Lutin/Lurette testing tool.
It is available on the Verimag website.
Purpose This proof-of-concept demo illustrates the use of a Abstract Interpretation tool (pagai) for finding infeasible paths in C programs. The goal is to enhance the Worst Case Execution Time (WCET) estimation, using the otawa framework for timing analysis.
It has been developed during the W-SEPT project.
Reference: Improving WCET Evaluation using Linear Relation Analysis. Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, Rémy (in Leibniz Transactions on Embedded Systems, 2019)
Purpose This proof-of-concept demo illustrates the use of a model checker (lesar) for finding infeasible paths in a synchronous code (written in lustre). The goal is to enhance the Worst Case Execution Time (WCET) estimation, using the otawa framework for timing analysis.
It has been developed during the W-SEPT project.
Reference: Timing analysis enhancement for synchronous program. Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Carrier, Fabienne and Asavoae, Mihail (in Real-Time Systems, 2015)
