jasmin
jasmin copied to clipboard
more flexibility for (s)ct checker
The main idea of this PR is do provide more flexibility in the usage of (S)CT checker. What we want is to be able to add annotations in libjade allowing to say if (export) functions are CT of SCT. By default, function export in libjade should be at least CT, but we want to be able replace step by step some CT implementations by SCT one (and this should be clearly expressed in the file). We also want to have the possibility to provide two implementations in particular in the case where the SCT version is much more costly.
For a longer term, I would like to be able to automatically print header file (for C for exemple), and I would like to be sure that the printed annotation are corrects (so we will need to check it before printing). To do that, it will be good to be able to add safety annotation directly in the jazz file. As well as functions documentation that can be also propagated to header file.